#include <ctime>
#include "types.hh"
#include "utilities.hh"

using namespace std;

basictype::basictype(string *n)
{
    name = n;
    type = 1;
    index_begin = -1;
    index_end = -1;
    is_add_built = false;
}
basictype::basictype(string *n, unsigned char t)
{
    name = n;
    type = t;
    index_begin = -1;
    index_end = -1;
    is_add_built = false;
}
basictype::~basictype()
{
    cout << "deleting basictype " << to_string() << endl;
    delete name;
}

string basictype::get_name()
{
    if (name == NULL)
    {
        cout << "type name is unknown" << endl;
        exit(1);
    }
    return *name;
}

unsigned char basictype::get_type()
{
    return type;
}

string basictype::to_string()
{
    return *name + ": boolean";
}

int basictype::BDD_length()
{
    return 1;
}

void basictype::set_index_begin(int i)
{
    index_begin = i;
}

void basictype::set_index_end(int i)
{
    index_end = i;
}
int basictype::get_index_begin()
{
    return index_begin;
}

int basictype::get_index_end()
{
    return index_end;
}
void basictype::print_value_index()
{
    cout << "true: 1" << endl;
    cout << "false: 0" << endl;
}
void basictype::print_state(string prefix, BDD state, BDDvector v)
{
    cout << prefix << *name << " = ";
    if (state <= v[index_begin])
        cout << "true";
    else
        cout << "false";
}

void basictype::print_stateXML(ofstream* myfile, BDD state, BDDvector v)
{
    *myfile << "        <variable name=\"" << *name << "\">";
    if (state <= v[index_begin])
        *myfile << "true";
    else
        *myfile << "false";
    *myfile << "</variable>\n";
}

string basictype::state_to_str(BDD state, BDDvector v)
{
    ostringstream s;
    s << *name << "=";
    if (state <= v[index_begin])
        s << "true";
    else
        s << "false";
    return s.str();
}

bool basictype::is_valid_state(BDD state, BDDvector v)
{
    return true;
}

ADD basictype::build_ADD_tree()
{
    if (is_add_built)
        return add_tree;
    int index_begin = get_index_begin();
    add_tree = ((*addv)[index_begin] * bddmgr->constant(1))
            + (~(*addv)[index_begin] * bddmgr->constant(0));
    is_add_built = true;
    return add_tree;
}

BDD basictype::build_all_BDDs()
{
    return bddmgr->bddOne();
}

enumerate::enumerate(string *n, set<string> *s) :
    basictype(n, 3)
{
    enumvalue = s;
    value_index = new map<string, vector<bool>*> ;
    bdd_length = enumvalue == NULL ? 0 : log_2(enumvalue->size());
    set_value_index();
    is_add_built = false;
}
enumerate::~enumerate()
{
    cout << "deleting enumerate " << to_string() << endl;
    delete enumvalue;
}
set<string> * enumerate::get_enumvalue()
{
    return enumvalue;
}

int enumerate::is_valid_value(string s)
{
    if (enumvalue == NULL)
    {
        cout << "enum list is unknown" << endl;
        exit(1);
    }
    return (enumvalue->find(s) != enumvalue->end());
}
string enumerate::to_string()
{
    string str = ": { ";
    int k = 0;
    int j = enumvalue->size() - 1;
    for (set<string>::iterator i = enumvalue->begin(); i != enumvalue->end(); i++)
    {
        if (k == j)
            str += *i + " ";
        else
            str += *i + ", ";
        k++;
    }
    str += "}";
    return get_name() + str;
}

int enumerate::BDD_length()
{
    return bdd_length;
}

void enumerate::set_value_index()
{
    int size = BDD_length();
    vector<bool> base(size, false);
    for (set<string>::iterator i = enumvalue->begin(); i != enumvalue->end(); i++)
    {
        vector<bool>* temp = new vector<bool> (base);
        pair<string, vector<bool>*> p(*i, temp);
        value_index->insert(p);
        for (int j = size - 1; j >= 0; j--)
        {
            if (base[j])
                base[j] = false;
            else
            {
                base[j] = true;
                break;
            }
        }
    }
}
void enumerate::print_value_index()
{
    for (map<string, vector<bool>*>::iterator i = value_index->begin(); i
            != value_index->end(); i++)
    {
        cout << i->first << ": ";
        for (unsigned int j = 0; j < i->second->size(); j++)
            cout << ((*(i->second))[j] ? 1 : 0);
        cout << endl;
    }
}
vector<bool>* enumerate::get_value_index(string value)
{
    if (value_index != NULL)
    {
        map<string, vector<bool>*>::iterator i = value_index->find(value);
        if (i != value_index->end())
            return i->second;
    }
    return NULL;
}

string enumerate::find_value_by_index(vector<bool> index)
{
    for (map<string, vector<bool>*>::iterator i = value_index->begin(); i
            != value_index->end(); i++)
    {
        bool flag = true;
        for (unsigned int j = 0; j < i->second->size(); j++)
            if ((*(i->second))[j] != index[j])
            {
                flag = false;
                break;
            }
        if (flag)
            return i->first;
    }
    return "";
}
void enumerate::print_state(string prefix, BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    cout << prefix << get_name() << " = ";
    //cout.flush();
    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    string value = find_value_by_index(index);
    cout << value;
    /*  for(map<string, vector<bool>* >::iterator i=value_index->begin(); i!=value_index->end(); i++) {
     bool flag = true;
     for(unsigned int j=0; j<i->second->size(); j++)
     if((*(i->second))[j] != index[j]) {
     flag = false;
     break;
     }
     if(flag)
     cout << i->first;
     }
     */
}
void enumerate::print_stateXML(ofstream* myfile, BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    *myfile << "        <variable name=\"" << get_name() << "\">";

    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    string value = find_value_by_index(index);
    *myfile << value;
    *myfile << "</variable>\n";
}

string enumerate::state_to_str(BDD state, BDDvector v)
{
    ostringstream s;
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    s << get_name() << "=";

    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    string value = find_value_by_index(index);
    s << value;
    return s.str();
}

bool enumerate::is_valid_state(BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    string value = find_value_by_index(index);
    if (value == "")
        return false;
    else
        return true;
}

ADD enumerate::build_ADD_tree()
{
    if (is_add_built)
        return add_tree;
    int index_begin = get_index_begin();
    add_tree = bddmgr->addZero();
    int index = 1;
    for (set<string>::iterator i = enumvalue->begin(); i != enumvalue->end(); i++)
    {
        vector<bool>* v = get_value_index(*i);
        ADD path = bddmgr->constant(index);
        index++;
        for (unsigned int j = 0; j < v->size(); j++)
            if ((*v)[j])
                path *= (*addv)[index_begin + j];
            else
                path *= ~(*addv)[index_begin + j];
        add_tree += path;
    }
    is_add_built = true;
    return add_tree;
}

BDD enumerate::build_all_BDDs()
{
    unsigned int length = 1;
    length <<= bdd_length;
    //cout << "length = " << length << endl;
    if (enumvalue->size() < length)
    {
        int index_begin = get_index_begin();
        BDD bdd_tree = bddmgr->bddZero();
        int index = 1;
        for (set<string>::iterator i = enumvalue->begin(); i
                != enumvalue->end(); i++)
        {
            vector<bool>* vindex = get_value_index(*i);
            BDD path = bddmgr->bddOne();
            index++;
            for (unsigned int j = 0; j < vindex->size(); j++)
                if ((*vindex)[j])
                    path *= (*v)[index_begin + j];
                else
                    path *= ~(*v)[index_begin + j];
            bdd_tree += path;
        }
        //cout << to_string();
        //bdd_tree.print(2, 2);
        return bdd_tree;
    }
    else
        return bddmgr->bddOne();
}

rangedint::rangedint(string *n, int l, int u) :
    basictype(n, 2)
{
    lowerbound = l;
    upperbound = u;
    bdd_length = log_2(upperbound - lowerbound + 1);
    power_two = 1;
    power_two = power_two << bdd_length;
    half_power = 1;
    half_power = half_power << (bdd_length - 1);
    half_power += lowerbound;
    is_add_built = false;
}
rangedint::~rangedint()
{
    cout << "deleting rangedint " << to_string() << endl;
}
int rangedint::get_lowerbound()
{
    return lowerbound;
}
int rangedint::get_upperbound()
{
    return upperbound;
}

bool rangedint::is_valid_value(int i)
{
    return (i <= upperbound && i >= lowerbound);
}
string rangedint::to_string()
{
    ostringstream o, p;
    o << lowerbound;
    p << upperbound;
    return get_name() + ": " + o.str() + " .. " + p.str();
}
int rangedint::BDD_length()
{
    return bdd_length;
}
void rangedint::print_value_index()
{
    for (int k = lowerbound; k <= upperbound; k++)
    {
        cout << k << ": ";
        vector<int>* v = get_value_index(k);
        for (unsigned int j = 0; j < v->size(); j++)
            cout << ((*v)[j] == 1 ? "1" : ((*v)[j] == -1 ? "0" : "_"));
        cout << endl;
    }
}
vector<int>* rangedint::get_value_index(int value)
{
    if (value >= lowerbound && value <= upperbound)
    {
        //int index_end = get_index_end();
        vector<int> *temp = new vector<int> (bdd_length, -1);
        if (power_two + lowerbound == upperbound + 1)
        {
            int distance = value - lowerbound;
            for (int i = bdd_length - 1; i >= 0; i--)
            {
                if ((distance & 1) == 1)
                    (*temp)[i] = 1;
                distance >>= 1;
            }
        }
        else
        {
            int index = value - half_power;
            if (index < 0)
            {
                int distance = value - lowerbound;
                for (int i = bdd_length - 2; i >= 0; i--)
                {
                    if ((distance & 1) == 1)
                        (*temp)[i] = 1;
                    distance >>= 1;
                }
                if (value - lowerbound > upperbound - half_power)
                    (*temp)[bdd_length - 1] = 0;
            }
            else
            {
                int distance = index;
                for (int i = bdd_length - 2; i >= 0; i--)
                {
                    if ((distance & 1) == 1)
                        (*temp)[i] = 1;
                    distance >>= 1;
                }
                (*temp)[bdd_length - 1] = 1;
            }
        }
        return temp;
    }
    return NULL;
}

int rangedint::find_value_by_index(vector<bool> index)
{
    int value = 0;
    if (power_two + lowerbound == upperbound + 1)
    {
        for (unsigned int i = 0; i < index.size(); i++)
        {
            value <<= 1;
            value += (index[i] == true ? 1 : 0);
        }
        return value + lowerbound;
    }
    else
    {
        for (unsigned int i = 0; i < index.size() - 1; i++)
        {
            value <<= 1;
            value += (index[i] == true ? 1 : 0);
        }
        if (value > upperbound - half_power || index[bdd_length - 1] == false)
            return value + lowerbound;
        else
            return value + half_power;
    }
}

void rangedint::print_state(string prefix, BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    cout << prefix << get_name() << " = ";
    //cout.flush();
    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    int value = find_value_by_index(index);
    cout << value;
    /*int value = 0;
     for(int i=0; i<index.size(); i++) {
     value <<= 1;
     value += (index[i]==true? 1 : 0);
     }
     cout << value+lowerbound;*/
}

void rangedint::print_stateXML(ofstream* myfile, BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();

    *myfile << "        <variable name=\"" << get_name() << "\">";

    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    int value = find_value_by_index(index);
    *myfile << value;
    *myfile << "</variable>\n";

}

string rangedint::state_to_str(BDD state, BDDvector v)
{
    ostringstream s;
    int index_begin = get_index_begin();
    int index_end = get_index_end();

    s << get_name() << "=";

    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    int value = find_value_by_index(index);
    s << value;
    return s.str();
}

bool rangedint::is_valid_state(BDD state, BDDvector v)
{
    int index_begin = get_index_begin();
    int index_end = get_index_end();
    vector<bool> index;
    for (int i = index_begin; i <= index_end; i++)
        if (state <= v[i])
            index.push_back(true);
        else
            index.push_back(false);
    int value = find_value_by_index(index);
    if (value > upperbound)
        return false;
    else
        return true;
}
ADD rangedint::build_ADD_tree()
{
    if (is_add_built)
        return add_tree;
    int index_begin = get_index_begin();
    add_tree = bddmgr->addZero();
    for (int i = lowerbound; i <= upperbound; i++)
    {
        vector<int>* v = get_value_index(i);
        ADD path = bddmgr->constant(i);
        for (unsigned int j = 0; j < v->size(); j++)
            if ((*v)[j] == 1)
                path *= (*addv)[index_begin + j];
            else if ((*v)[j] == -1)
                path *= ~(*addv)[index_begin + j];
        add_tree += path;
    }
    is_add_built = true;
    return add_tree;
}

BDD rangedint::build_all_BDDs()
{
    return bddmgr->bddOne();
}

Object::~Object()
{
}
string Object::to_string()
{
    return "";
}

expression::expression(unsigned char i)
{
    type = i;
}

expression::~expression()
{
}
unsigned char expression::get_type()
{
    return type;
}
string expression::to_string()
{
    return "";
}
ADD expression::build_ADD_tree()
{
    return bddmgr->addZero();
}
bool expression::equal_to(expression *expr)
{
    return type == expr->get_type();
}

variable::variable(string *a_n, string *n) :
    expression(0)
{
    agent_name = a_n;
    name = n;
    var_type = NULL;
}
variable::variable(string *n) :
    expression(0)
{
    agent_name = NULL;
    name = n;
    var_type = NULL;
}
variable::variable(string *a_n, string *n, basictype *v_t) :
    expression(0)
{
    agent_name = a_n;
    name = n;
    var_type = v_t;
}
variable::~variable()
{
    cout << "deleting variable " << to_string() << endl;
    //delete agent_name;
    //delete name;
}
bool variable::equal_to(variable *expr)
{
    if (agent_name == NULL && expr->is_agent_name_null())
        return (name->compare(expr->get_variable_name())) == 0;
    else if (agent_name != NULL && !expr->is_agent_name_null())
        return ((name->compare(expr->get_variable_name())) == 0)
                && ((agent_name->compare(expr->get_agent_name())) == 0);
    return false;
}
bool variable::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((variable *) expr);
    return false;
}

void variable::set_agent_name(string *a_n)
{
    agent_name = a_n;
}
string variable::get_agent_name()
{
    if (agent_name == NULL)
    {
        cout << "error: the agent name of the given variable is undefined!"
                << endl;
        exit(1);
    }
    else
        return *agent_name;
}
string* variable::get_variable_name_point()
{
    return name;
}
bool variable::is_agent_name_null()
{
    return agent_name == NULL;
}
string variable::get_variable_name()
{
    if (name == NULL)
    {
        cout << "error: the name of the given variable is undefined!" << endl;
        exit(1);
    }
    else
        return *name;
}
string variable::to_string()
{
    return (agent_name == NULL ? "" : *agent_name + ".") + get_variable_name();
}
void variable::set_var_type(basictype *t)
{
    var_type = t;
}
basictype* variable::get_var_type()
{
    return var_type;
}
ADD variable::build_ADD_tree()
{
    if (var_type == NULL)
    {
        if (options["quiet"] == 0)
            cout << "Warning: var_type in " << to_string() << " is NULL"
                    << endl;
        return bddmgr->addZero();
    }
    if (var_type->get_type() == 2)
        return ((rangedint *) var_type)->build_ADD_tree();
    else
        return bddmgr->addZero();
}
variable* variable::permute_agents(map<string, string> *permutation)
{
    basic_agent *lagent_new = (*is_agents)[(*permutation)[*agent_name]];
    basictype *lvar_type_new = lagent_new->get_basictype_by_name(*name);
    return new variable(lagent_new->get_name_point(), name, lvar_type_new);
}

laction::laction() :
    expression(4)
{
    agent_name = NULL;
    agent = NULL;
}
laction::laction(string *a_n) :
    expression(4)
{
    agent_name = a_n;
    agent = NULL;
}
laction::laction(string *a_n, basic_agent *ag) :
    expression(4)
{
    agent_name = a_n;
    agent = ag;
}

laction::~laction()
{
    cout << "deleting laction " << to_string() << endl;
    //delete agent_name;
}

bool laction::equal_to(laction *expr)
{
    if (agent_name == NULL && expr->is_agent_name_null())
        return true;
    if (agent_name != NULL && !expr->is_agent_name_null())
        return agent_name->compare(expr->get_agent_name()) == 0;
    return false;
}
bool laction::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((laction *) expr);
    return false;
}

void laction::set_agent_name(string *a_n)
{
    agent_name = a_n;
}
string laction::get_agent_name()
{
    if (agent_name == NULL)
    {
        cout << "agent name in laction is unknown!" << endl;
        exit(1);
    }
    else
        return *agent_name;
}

void laction::set_agent(basic_agent* a)
{
    agent = a;
}
basic_agent* laction::get_agent()
{
    return agent;
}

bool laction::is_agent_name_null()
{
    return agent_name == NULL;
}
string laction::to_string()
{
    return (agent_name == NULL ? "" : *agent_name + ".") + "Action";
    //return "Action";
}
ADD laction::build_ADD_tree()
{
    return bddmgr->addZero();
}
laction* laction::permute_agents(map<string, string> *permutation)
{
    basic_agent *lagent_new = (*is_agents)[(*permutation)[*agent_name]];
    return new laction(lagent_new->get_name_point(), lagent_new);
}

bool_value::bool_value(bool v) :
    expression(1)
{
    value = v;
}
bool_value::~bool_value()
{
    cout << "deleting bool_value " << to_string() << endl;
}
bool bool_value::equal_to(bool_value *expr)
{
    return value == expr->get_value();
}
bool bool_value::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((bool_value *) expr);
    return false;
}
bool bool_value::get_value()
{
    return value;
}
string bool_value::to_string()
{
    return (value ? "true" : "false");
}
ADD bool_value::build_ADD_tree()
{
    if (value)
        return bddmgr->addOne();
    else
        return bddmgr->addZero();
}

int_value::int_value(int v) :
    expression(2)
{
    value = v;
}
int_value::~int_value()
{
    cout << "deleting int_value " << to_string() << endl;
}
bool int_value::equal_to(int_value *expr)
{
    return value == expr->get_value();
}
bool int_value::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((int_value *) expr);
    return false;
}

int int_value::get_value()
{
    return value;
}
string int_value::to_string()
{
    ostringstream o;
    o << value;
    return o.str();
}
ADD int_value::build_ADD_tree()
{
    return bddmgr->constant(value);
}

enum_value::enum_value(string *v) :
    expression(3)
{
    value = v;
}
enum_value::~enum_value()
{
    cout << "deleting enum_value " << to_string() << endl;
    //delete value;
}
bool enum_value::equal_to(enum_value *expr)
{
    return value->compare(expr->get_value()) == 0;
}
bool enum_value::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((enum_value *) expr);
    return false;
}
string enum_value::get_value()
{
    if (value == NULL)
    {
        cout << "enum value is unknown!" << endl;
        exit(1);
    }
    else
        return *value;
}
string enum_value::to_string()
{
    return get_value();
}
ADD enum_value::build_ADD_tree()
{
    return bddmgr->addZero();
}

/**********************************************
 arithmetic_expression
 **********************************************/
arithmetic_expression::arithmetic_expression(unsigned char o, expression *e1,
        expression *e2) :
    expression(o)
{
    operands[0] = e1;
    operands[1] = e2;
}
arithmetic_expression::~arithmetic_expression()
{
    cout << "deleting arithmetic_expression " << to_string() << endl;
    //delete []operands;
}
expression* arithmetic_expression::get_operand(unsigned char i)
{
    if (i > 1)
    {
        cout << "error: arithmetic operand " << i << " does not exist!" << endl;
        exit(1);
    }
    else if (operands[i] == NULL)
    {
        cout << "error: arithmetic operand " << i << " is undefined!" << endl;
        exit(1);
    }
    else
        return (operands[i]);
}
bool arithmetic_expression::equal_to(arithmetic_expression *expr)
{
    unsigned int op = get_type();
    if (op == expr->get_type())
        return ((expression *) (operands[0]))->equal_to(expr->get_operand(0))
                && ((expression *) (operands[1]))->equal_to(
                        expr->get_operand(1));

    return false;
}
bool arithmetic_expression::equal_to(expression *expr)
{
    if (expr->get_type() == get_type())
        return equal_to((arithmetic_expression *) expr);
    return false;
}

string arithmetic_expression::to_string()
{
    string opstr;
    unsigned int op = get_type();
    if (op == 0)
        return ((expression *) (operands[0]))->to_string();
    else if (op == 5)
        opstr = "+";
    else if (op == 6)
        opstr = "-";
    else if (op == 7)
        opstr = "*";
    else if (op == 8)
        opstr = "/";
    return ((expression *) (operands[0]))->to_string() + " " + opstr + " "
            + ((expression *) (operands[1]))->to_string();
}

/*bool arithmetic_expression::check_var_and_value(map<string, basictype *> *vars) {
 bool flag = true;
 unsigned char left = operands[0]->get_type(); // left hand side
 unsigned char right = operands[1]->get_type(); // right hand side
 if(left==0) {// left hand side is a variable
 string vs = ((variable *)operands[0])->get_variable_name();
 map<string, basictype *>::iterator p = vars->find(vs);
 if(p==vars->end()) {
 cout << "        variable " << vs << " is not defined." << endl;
 flag = false;
 } else
 ((variable *)operands[0])->set_var_type(p->second);
 } else if(left>=5 && left<=8) {//lhs is an arithmetic expression
 flag = ((arithmetic_expression*)operands[0])->check_var_and_value(vars);
 } else if(left!=2) { // lhs is not an integer
 cout<< "        left hand side in" << to_string() << " has a wrong type." << endl;
 flag = false;
 }

 if(right==0) {// right hand side is a variable
 string vs1 = ((variable *)operands[1])->get_variable_name();
 map<string, basictype *>::iterator p1 = vars->find(vs1);
 if(p1==vars->end()) {
 cout << "        variable " << vs1 << " is not defined." << endl;
 flag = false;
 } else
 ((variable *)operands[1])->set_var_type(p1->second);
 } else if(right>=5 && right<=8) {//lhs is an arithmetic expression
 flag = ((arithmetic_expression*)operands[1])->check_var_and_value(vars) && flag;
 } else if(right!=2) { // lhs is not an integer
 cout<< "        right hand side in" << to_string() << " has a wrong type." << endl;
 flag = false;
 }
 return flag;
 }*/

bool arithmetic_expression::check_var_and_value(
        map<string, basictype *> *obsvars, map<string, basictype *> *vars)
{
    bool flag = true;
    unsigned char left = operands[0]->get_type(); // left hand side
    unsigned char right = operands[1]->get_type(); // right hand side
    if (left == 0)
    {// left hand side is a variable
        variable * var = (variable *) operands[0];
        string vs = var->get_variable_name();
        if (var->is_agent_name_null())
        {
            map<string, basictype *>::iterator p = vars->find(vs);
            if (p == vars->end())
            {
                cout << "        variable " << vs << " is not defined." << endl;
                flag = false;
            }
            else
                var->set_var_type(p->second);
        }
        else if (var->get_agent_name() == "Environment")
        {
            map<string, basictype *>::iterator p = obsvars->find(vs);
            if (p == obsvars->end())
            {
                cout << "        variable " << vs << " is not defined." << endl;
                flag = false;
            }
            else
                var->set_var_type(p->second);
        }
        else
        {
            cout << "        variable " << vs << " is not defined." << endl;
            flag = false;
        }
    }
    else if (left >= 5 && left <= 8)
    {//lhs is an arithmetic expression
        flag = ((arithmetic_expression*) operands[0])->check_var_and_value(
                obsvars, vars);
    }
    else if (left != 2)
    { // lhs is not an integer
        cout << "        left hand side in" << to_string()
                << " has a wrong type." << endl;
        flag = false;
    }

    if (right == 0)
    {// right hand side is a variable
        variable * var = (variable *) operands[1];
        string vs = var->get_variable_name();
        if (var->is_agent_name_null())
        {
            map<string, basictype *>::iterator p = vars->find(vs);
            if (p == vars->end())
            {
                cout << "        variable " << vs << " is not defined." << endl;
                flag = false;
            }
            else
                var->set_var_type(p->second);
        }
        else if (var->get_agent_name() == "Environment")
        {
            map<string, basictype *>::iterator p = obsvars->find(vs);
            if (p == obsvars->end())
            {
                cout << "        variable " << vs << " is not defined." << endl;
                flag = false;
            }
            else
                var->set_var_type(p->second);
        }
        else
        {
            cout << "        variable " << vs << " is not defined." << endl;
            flag = false;
        }
    }
    else if (right >= 5 && right <= 8)
    {//lhs is an arithmetic expression
        flag = ((arithmetic_expression*) operands[1])->check_var_and_value(
                obsvars, vars) && flag;
    }
    else if (right != 2)
    { // lhs is not an integer
        cout << "        right hand side in" << to_string()
                << " has a wrong type." << endl;
        flag = false;
    }
    return flag;
}

bool arithmetic_expression::check_var_and_value(map<string, map<string,
        basictype *> > *vars)
{
    bool flag = true;
    unsigned char left = operands[0]->get_type(); // left hand side
    unsigned char right = operands[1]->get_type(); // right hand side
    if (left == 0)
    {// left hand side is a variable
        variable * var = (variable *) operands[0];
        string vs = var->get_variable_name();
        string ag_name = var->get_agent_name();
        map<string, map<string, basictype *> >::iterator gp = vars->find(
                ag_name);
        if (gp == vars->end())
        {
            cout << "    undefined agent " << ag_name << endl;
            return false;
        }
        map<string, basictype *>::iterator p = gp->second.find(vs);
        if (p == gp->second.end())
        {
            cout << "        variable " << vs << " is not defined in agent "
                    << ag_name << endl;
            flag = false;
        }
        else
            var->set_var_type(p->second);
    }
    else if (left >= 5 && left <= 8)
    {//lhs is an arithmetic expression
        flag
                = ((arithmetic_expression*) operands[0])->check_var_and_value(
                        vars);
    }
    else if (left != 2)
    { // lhs is not an integer
        cout << "        left hand side in" << to_string()
                << " has a wrong type." << endl;
        flag = false;
    }

    if (right == 0)
    {// right hand side is a variable
        variable * var1 = (variable *) operands[1];
        string vs1 = var1->get_variable_name();
        string ag_name = var1->get_agent_name();
        map<string, map<string, basictype *> >::iterator gp = vars->find(
                ag_name);
        if (gp == vars->end())
        {
            cout << "    undefined agent " << ag_name << endl;
            return false;
        }
        map<string, basictype *>::iterator p = gp->second.find(vs1);
        if (p == gp->second.end())
        {
            cout << "        variable " << vs1 << " is not defined in agent "
                    << ag_name << endl;
            flag = false;
        }
        else
            var1->set_var_type(p->second);
    }
    else if (right >= 5 && right <= 8)
    {//lhs is an arithmetic expression
        flag
                = ((arithmetic_expression*) operands[1])->check_var_and_value(
                        vars) && flag;
    }
    else if (right != 2)
    { // lhs is not an integer
        cout << "        right hand side in" << to_string()
                << " has a wrong type." << endl;
        flag = false;
    }
    return flag;
}

ADD arithmetic_expression::build_ADD_tree()
{
    unsigned char op = get_type();
    ADD res;
    ADD lhs = operands[0]->build_ADD_tree();
    ADD rhs = operands[1]->build_ADD_tree();
    if (op == 5)
    { // plus
        res = lhs + rhs;
    }
    else if (op == 6)
    { // minus
        res = lhs - rhs;
    }
    else if (op == 7)
    { // times
        res = lhs * rhs;
    }
    else
    { // divide
        res = lhs.Divide(rhs);
    }
    return res;
}

arithmetic_expression* arithmetic_expression::permute_agents(
        map<string, string> *permutation)
{
    unsigned char left = operands[0]->get_type(); // left hand side
    unsigned char right = operands[1]->get_type(); // right hand side
    expression
            * lexpr =
                    left == 0 ? ((variable *) operands[0])->permute_agents(
                            permutation)
                            : ((left >= 5 && left <= 8) ? ((arithmetic_expression*) operands[0])->permute_agents(
                                    permutation)
                                    : operands[0]);
    expression
            * rexpr =
                    right == 0 ? ((variable *) operands[1])->permute_agents(
                            permutation)
                            : ((right >= 5 && right <= 8) ? ((arithmetic_expression*) operands[1])->permute_agents(
                                    permutation)
                                    : operands[1]);
    return new arithmetic_expression(get_type(), lexpr, rexpr);
}

/**********************************************
 logic_expression
 **********************************************/
logic_expression::logic_expression(unsigned char o, expression *e1,
        expression *e2)
{
    op = o;
    operands[0] = e1;
    operands[1] = e2;
}
logic_expression::~logic_expression()
{
    cout << "deleting logic_expression " << to_string() << endl;
    //delete []operands;
}
unsigned char logic_expression::get_op()
{
    return op;
}
expression* logic_expression::get_operand(unsigned char i)
{
    if (i > 1)
    {
        cout << "error: logic operand " << i << " does not exist!" << endl;
        exit(1);
    }
    else if (operands[i] == NULL)
    {
        cout << "error: logic operand " << i << " is undefined!" << endl;
        exit(1);
    }
    else
        return (operands[i]);
}
bool logic_expression::equal_to(logic_expression *expr)
{
    if (op == expr->get_op()) /*{
     unsigned int left1 = ((expression *)(operands[0]))->get_type();
     unsigned int right1 = ((expression *)(operands[1]))->get_type();
     unsigned int left2 = ((expression *)expr->get_operand(0))->get_type();
     unsigned int right2 = ((expression *)expr->get_operand(0))->get_type();
     if(left1 == left2 && right1==right2) {
     bool result1 = true;
     bool result2 = true;
     switch(
     }
     }*/
        return ((expression *) (operands[0]))->equal_to(expr->get_operand(0))
                && ((expression *) (operands[1]))->equal_to(
                        expr->get_operand(1));

    return false;
}

string logic_expression::to_string()
{
    string opstr;
    if (op == 0)
        opstr = "=";
    else if (op == 1)
        opstr = "<>";
    else if (op == 2)
        opstr = "<";
    else if (op == 3)
        opstr = "<=";
    else if (op == 4)
        opstr = ">";
    else if (op == 5)
        opstr = ">=";
    return ((expression *) (operands[0]))->to_string() + opstr
            + ((expression *) (operands[1]))->to_string();
}

/*bool logic_expression::check_var_and_value(map<string, basictype *> *vars) {
 unsigned char left = operands[0]->get_type(); // left hand side
 unsigned char right = operands[1]->get_type(); // right hand side
 bool left_var = true;
 bool right_var = true;

 if(left==0) {// left hand side is a variable, or an enumerate value
 string vs = ((variable *)operands[0])->get_variable_name();
 map<string, basictype *>::iterator p = vars->find(vs);
 if(p==vars->end())
 left_var = false;
 if(right==0) {// right hand side could be a variable or a enumerate value
 string vs1 = ((variable *)operands[1])->get_variable_name();
 map<string, basictype *>::iterator p1 = vars->find(vs1);
 if(p1==vars->end())
 right_var = false;
 if(left_var && right_var) {// both sides are variables
 //check if both sides have the same type.
 unsigned char t1 = p->second->get_type(); //lhs' type
 unsigned char t2 = p1->second->get_type(); //rhs' type
 if(t1 == t2) { // same type
 if(t1==3) {// enumerate type
 //check if operation over the two variables is equal or nonequal test
 if(op!=0 && op!=1) {
 cout << "        only '=' and '<>' are allowed for enumeration variables." << endl;
 return false;
 }
 set<string> * s1 = ((enumerate *)(p->second))->get_enumvalue();
 set<string> * s2 = ((enumerate *)(p1->second))->get_enumvalue();
 if(s1->size()==s2->size()) {// same size
 bool equal = true;
 for(set<string>::iterator i=s1->begin(); i!=s1->end(); i++)
 if(s2->find(*i)==s2->end()) {
 equal = false;
 break;
 }
 if(equal) {
 // add a link in variable to its type
 ((variable *)operands[0])->set_var_type(p->second);
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 } else {
 cout << "        " << vs << " and " << vs1 << " do not have the same enumeration type." << endl;
 return false;
 }
 } else {
 cout << "        " << vs << " and " << vs1 << " do not have the same enumeration type." << endl;
 return false;
 }
 } else {
 if(t1==1 && op!=0 && op!=1) {
 cout << "        only '=' and '<>' are allowed for boolean variables." << endl;
 return false;
 }
 ((variable *)operands[0])->set_var_type(p->second);
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 }
 } else {
 cout << "        " << vs << " and " << vs1 << " have different type." << endl;
 return false;
 }
 } else if(left_var && !right_var) {// lhs is a variable and rhs is an enumeration value
 if(op!=0 && op!=1) {
 cout << "        only '=' and '<>' are allowed for enumeration variables." << endl;
 return false;
 }
 unsigned char t1 = p->second->get_type(); //lhs' type
 if(t1==3) {// lhs must be enumerate
 set<string> * s1 = ((enumerate *)(p->second))->get_enumvalue();
 if(s1->find(vs1)!=s1->end()) {//find a matched value in the enumeration type
 // add a link in lhs to its type
 ((variable *)operands[0])->set_var_type(p->second);
 //change the rhs to be an enumerate value
 operands[1] = new enum_value(new string(vs1));
 return true;
 } else {
 cout << "        " << vs << " does not have the value " << vs1 << endl;
 return false;
 }
 } else {
 cout << "        " << vs << " must have an enumerate type." << endl;
 return false;
 }
 } else if(!left_var && right_var) {// lhs is an enumeration value and rhs is a variable
 if(op!=0 && op!=1) {
 cout << "        only '=' and '<>' are allowed for enumeration variables." << endl;
 return false;
 }
 unsigned char t2 = p1->second->get_type(); //rhs' type
 if(t2==3) {// rhs must be enumerate
 set<string> * s2 = ((enumerate *)(p1->second))->get_enumvalue();
 if(s2->find(vs)!=s2->end()) {//find a matched value in the enumeration type
 // add a link in rhs to its type
 ((variable *)operands[1])->set_var_type(p1->second);
 //change the lhs to be an enumerate value
 operands[0] = new enum_value(new string(vs));
 return true;
 } else {
 cout << "        " << vs1 << " does not have the value " << vs << endl;
 return false;
 }
 } else {
 cout << "        " << vs1 << " must have an enumeration type." << endl;
 return false;
 }
 } else {
 cout << "        " << vs << " or " << vs1 << " must be a variable." << endl;
 return false;
 }
 } else if(left_var){
 left = p->second->get_type();
 if(right==1) {// right hand side is a boolean value
 if(left != 1) {
 cout << "         " << vs << " in " << to_string() << " is not a Boolean variable." << endl;
 return false;
 }
 if(op==0 || op==1) {// only equality is allowed here
 // add a link in variable to its type
 ((variable *)operands[0])->set_var_type(p->second);
 return true;
 } else {
 cout << "        only equality or inequality test is allowed in " << to_string() << "." << endl;
 return false;
 }
 } else if(right==2) {// right hand side is an integer
 if(left != 2) {
 cout << "         " << vs << " in " << to_string() << " is not a bounded integer variable." << endl;
 return false;
 }
 ((variable *)operands[0])->set_var_type(p->second);
 return true;
 } else if(right==3) {// right hand side is an enumerate value. It cannot happen. But we still check it.
 cout<< "        enumerate value cannot appear here." << endl;
 if(left != 3) {
 cout << "         " << vs << " in " << to_string() << " is not an enumeration variable." << endl;
 return false;
 }
 if(op==0 || op==1) {// only equality is allowed here
 string vs1 = ((enum_value *)operands[1])->get_value();
 set<string> * s1 = ((enumerate *)(p->second))->get_enumvalue();
 if(s1->find(vs1)!=s1->end()) {//find a matched value in the enumerate type
 // add a link in lhs to its type
 ((variable *)operands[0])->set_var_type(p->second);
 return true;
 } else {
 cout << "        " << vs << " does not have the value " << vs1 << endl;
 return false;
 }
 } else {
 cout << "        only equality or inequality test is allowed in " << to_string() << "." << endl;
 return false;
 }
 } else {// right hand side is an arithmetic expression
 if(p->second->get_type()==2 &&
 ((arithmetic_expression *)operands[1])->check_var_and_value(vars)){
 // add a link in lhs to its type
 ((variable *)operands[0])->set_var_type(p->second);
 return true;
 } else {
 cout << "        " << vs << "does not have integer type or " <<
 ((arithmetic_expression *)operands[1])->to_string() <<
 " is not a correct arithmetic expression." << endl;
 return false;
 }
 }
 } else {
 cout << "        " << vs << " must be a variable." << endl;
 return false;
 }
 } else if(right==0) {// right hand side is a variable
 string vs1 = ((variable *)operands[1])->get_variable_name();
 map<string, basictype *>::iterator p1 = vars->find(vs1);
 if(p1!=vars->end()) {
 right = p1->second->get_type();
 if(left==1) {// left hand side is a boolean value
 if(right != 1) {
 cout << "         " << vs1 << " in " << to_string() << " is not a Boolean variable." << endl;
 return false;
 }
 if(op==0 || op==1) {// only equality is allowed here
 // add a link in variable to its type
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 } else {
 cout << "        only equality or inequality test is allowed in " << to_string() << "." << endl;
 return false;
 }
 } else if(left==2) {// left hand side is an integer
 if(right != 2) {
 cout << "         " << vs1 << " in " << to_string() << " is not a Boolean variable." << endl;
 return false;
 }
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 } else if(left==3) {// left hand side is an enumerate value. It cannot happen. But we still check it.
 if(right != 3) {
 cout << "         " << vs1 << " in " << to_string() << " is not a Boolean variable." << endl;
 return false;
 }
 cout<< "        enumerate value cannot appear here." << endl;
 if(op==0 || op==1) {// only equality is allowed here
 string vs = ((enum_value *)operands[0])->get_value();
 set<string> * s2 = ((enumerate *)(p1->second))->get_enumvalue();
 if(s2->find(vs)!=s2->end()) {//find a matched value in the enumerate type
 // add a link in lhs to its type
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 } else {
 cout << "        " << vs1 << " does not have the value " << vs << endl;
 return false;
 }
 } else {
 cout << "        only equality or inequality test is allowed in " << to_string() << "." << endl;
 return false;
 }
 } else {// left hand side is an arithmetic expression
 if(p1->second->get_type()==2 &&
 ((arithmetic_expression *)operands[0])->check_var_and_value(vars)){
 // add a link in lhs to its type
 ((variable *)operands[1])->set_var_type(p1->second);
 return true;
 } else {
 cout << "        " << vs1 << "does not have integer type or " <<
 ((arithmetic_expression *)operands[0])->to_string() <<
 " is not a correct arithmetic expression." << endl;
 return false;
 }
 }
 } else {
 cout << "        " << vs1 << " must be a variable." << endl;
 return false;
 }
 } else if(left>=5 && left<=8) { // left hand side is an arithmetic expression
 if(right==2) // rhs is an integer
 return ((arithmetic_expression *)operands[0])->check_var_and_value(vars);
 else if(right>=5 && right<=8) // rhs is an arithmetic expression
 return ((arithmetic_expression *)operands[0])->check_var_and_value(vars) &&
 ((arithmetic_expression *)operands[1])->check_var_and_value(vars);
 else {
 cout << "        right hand side in " << to_string() << " has a wrong type." << endl;
 return false;
 }
 } else if(right>=5 && right<=8) { //right  hand side is an arithmetic expression
 if(left==2) // lhs is an integer
 return ((arithmetic_expression *)operands[1])->check_var_and_value(vars);
 else {
 cout << "        left hand side in " << to_string() << " has a wrong type." << endl;
 return false;
 }
 }
 cout << "        wrong logic expression " << to_string() << endl;
 return false;
 }*/

bool logic_expression::check_evolution(map<string, basictype *> *obsvars, map<
        string, basictype *> *vars, string agent_name,
        map<string, basic_agent*> *global_actions)
{
    unsigned char left = operands[0]->get_type(); // left hand side
    unsigned char right = operands[1]->get_type(); // right hand side
    bool left_var = true;
    bool right_var = true;

    if (left == 4)
    {
        map<string, basic_agent*>::iterator p;
        string act_name = ((variable *) operands[1])->get_variable_name();
        bool f = ((laction *) operands[0])->is_agent_name_null();
        string ag_name = f ? agent_name
                : ((laction *) operands[0])->get_agent_name();

        /*if(f) // local action
         p = global_actions->find(agent_name);
         else
         p = global_actions->find(ag_name);*/
        p = global_actions->find(ag_name);
        if (p == global_actions->end())
        {
            cout << "        action " << act_name << " is not found in agent "
                    <<
                    //(f ? agent_name : ag_name) << endl;
                    ag_name << endl;
            return false;
        }

        if (f)
        {
            ((laction *) operands[0])->set_agent_name(new string(agent_name));
            ((laction *) operands[0])->set_agent((*p).second);
        }
        else
            ((laction *) operands[0])->set_agent((*p).second);

        set<string>* acts = (*p).second->get_actions();
        set<string>::iterator s = acts->find(act_name);
        if (s == acts->end())
        {
            cout << "        action " << act_name << " is not found in agent "
                    <<
                    //(f ? agent_name : ag_name) << endl;
                    ag_name << endl;
            return false;
        }
        else
            return true;
    }
    else if (left == 0)
    {// left hand side is a variable, or an enumerate value
        variable* v1 = ((variable *) operands[0]);
        string vs = v1->get_variable_name();
        map<string, basictype *>::iterator p;
        if (v1->is_agent_name_null())
        {// local variable
            p = vars->find(vs);
            if (p == vars->end())
                left_var = false;
        }
        else
        {
            p = obsvars->find(vs);
            if (p == obsvars->end())
                left_var = false;
        }
        if (right == 0)
        {// right hand side could be a variable or a enumerate value
            variable* v2 = ((variable *) operands[1]);
            string vs1 = v2->get_variable_name();
            map<string, basictype *>::iterator p1;
            if (v2->is_agent_name_null())
            {// local variable
                p1 = vars->find(vs1);
                if (p1 == vars->end())
                    right_var = false;
            }
            else
            {
                p1 = obsvars->find(vs1);
                if (p1 == obsvars->end())
                    right_var = false;
            }
            if (left_var && right_var)
            {// both sides are variables
                //check if both sides have the same type.
                unsigned char t1 = p->second->get_type(); //lhs' type
                unsigned char t2 = p1->second->get_type(); //rhs' type
                if (t1 == t2)
                { // same type
                    if (t1 == 3)
                    {// enumerate type
                        if (op != 0 && op != 1)
                        {
                            cout
                                    << "        only '=' and '<>' are allowed for enumeration variables."
                                    << endl;
                            return false;
                        }
                        set<string> * s1 =
                                ((enumerate *) (p->second))->get_enumvalue();
                        set<string> * s2 =
                                ((enumerate *) (p1->second))->get_enumvalue();
                        if (s1->size() == s2->size())
                        {// same size
                            bool equal = true;
                            for (set<string>::iterator i = s1->begin(); i
                                    != s1->end(); i++)
                                if (s2->find(*i) == s2->end())
                                {
                                    equal = false;
                                    break;
                                }
                            if (equal)
                            {
                                if (t1 == 1 && op != 0 && op != 1)
                                {
                                    cout
                                            << "        only '=' and '<>' are allowed for boolean variables."
                                            << endl;
                                    return false;
                                }
                                // add a link in variable to its type
                                ((variable *) operands[0])->set_var_type(
                                        p->second);
                                ((variable *) operands[1])->set_var_type(
                                        p1->second);
                                return true;
                            }
                            else
                            {
                                cout << "        " << vs << " and " << vs1
                                        << " do not have the same enumerate type."
                                        << endl;
                                return false;
                            }
                        }
                        else
                        {
                            cout << "        " << vs << " and " << vs1
                                    << " do not have the same enumerate type."
                                    << endl;
                            return false;
                        }
                    }
                    else
                    {
                        ((variable *) operands[0])->set_var_type(p->second);
                        ((variable *) operands[1])->set_var_type(p1->second);
                        return true;
                    }
                }
                else
                {
                    cout << "        " << vs << " and " << vs1
                            << " have different type." << endl;
                    return false;
                }
            }
            else if (left_var && !right_var)
            {// lhs is a variable and rhs is an enumerate value
                if (op != 0 && op != 1)
                {
                    cout
                            << "        only '=' and '<>' are allowed for enumeration variables."
                            << endl;
                    return false;
                }
                unsigned char t1 = p->second->get_type(); //lhs' type
                if (t1 == 3)
                {// lhs must be enumerate
                    set<string> * s1 =
                            ((enumerate *) (p->second))->get_enumvalue();
                    if (s1->find(vs1) != s1->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[0])->set_var_type(p->second);
                        //change the rhs to be an enumerate value
                        operands[1] = new enum_value(new string(vs1));
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs << " does not have the value "
                                << vs1 << endl;
                        return false;
                    }
                }
                else
                {
                    cout << "        " << vs << " must have an enumerate type."
                            << endl;
                    return false;
                }
            }
            else if (!left_var && right_var)
            {// lhs is an enumerate value and rhs is a variable
                if (op != 0 && op != 1)
                {
                    cout
                            << "        only '=' and '<>' are allowed for enumeration variables."
                            << endl;
                    return false;
                }
                unsigned char t2 = p1->second->get_type(); //rhs' type
                if (t2 == 3)
                {// rhs must be enumerate
                    set<string> * s2 =
                            ((enumerate *) (p1->second))->get_enumvalue();
                    if (s2->find(vs) != s2->end())
                    {//find a matched value in the enumerate type
                        // add a link in rhs to its type
                        ((variable *) operands[1])->set_var_type(p1->second);
                        //change the lhs to be an enumerate value
                        operands[0] = new enum_value(new string(vs));
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs1
                                << " does not have the value " << vs << endl;
                        return false;
                    }
                }
                else
                {
                    cout << "        " << vs1
                            << " must have an enumerate type." << endl;
                    return false;
                }
            }
            else
            {
                cout << "        " << vs << " or " << vs1
                        << " must be a variable." << endl;
                return false;
            }
        }
        else if (left_var)
        {
            left = p->second->get_type();
            if (right == 1)
            {// right hand side is a boolean value
                if (left != 1)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    // add a link in variable to its type
                    ((variable *) operands[0])->set_var_type(p->second);
                    return true;
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else if (right == 2)
            {// right hand side is an integer
                if (left != 2)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not a bounded integer variable." << endl;
                    return false;
                }
                /*int vs1 = ((int_value *)operands[1])->get_value();
                 if(((rangedint *)(p->second))->is_valid_value(vs1)) {// the value is in the correct range
                 // add a link in variable to its type
                 ((variable *)operands[0])->set_var_type(p->second);
                 return true;
                 } else {
                 cout << "        " << vs1 << " is out of bound in " << to_string() << "." << endl;
                 return false;
                 }*/
                ((variable *) operands[0])->set_var_type(p->second);
                return true;
            }
            else if (right == 3)
            {// right hand side is an enumerate value. It cannot happen. But we still check it.
                cout << "        enumerate value cannot appear here." << endl;
                if (left != 3)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not an enumeration variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    string vs1 = ((enum_value *) operands[1])->get_value();
                    set<string> * s1 =
                            ((enumerate *) (p->second))->get_enumvalue();
                    if (s1->find(vs1) != s1->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[0])->set_var_type(p->second);
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs << " does not have the value "
                                << vs1 << endl;
                        return false;
                    }
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else
            {// right hand side is an arithmetic expression
                if (p->second->get_type() == 2
                        && ((arithmetic_expression *) operands[1])->check_var_and_value(
                                obsvars, vars))
                {
                    // add a link in lhs to its type
                    ((variable *) operands[0])->set_var_type(p->second);
                    return true;
                }
                else
                {
                    cout << "        " << vs
                            << "does not have integer type or "
                            << ((arithmetic_expression *) operands[1])->to_string()
                            << " is not a correct arithmetic expression."
                            << endl;
                    return false;
                }
            }
        }
        else
        {
            cout << "        " << vs << " must be a variable." << endl;
            return false;
        }
    }
    else if (right == 0)
    {// right hand side is a variable
        variable* v2 = ((variable *) operands[1]);
        string vs1 = ((variable *) operands[1])->get_variable_name();
        map<string, basictype *>::iterator p1;
        if (v2->is_agent_name_null())
        {// local variable
            p1 = vars->find(vs1);
            if (p1 == vars->end())
                right_var = false;
        }
        else
        {
            p1 = obsvars->find(vs1);
            if (p1 == obsvars->end())
                right_var = false;
        }
        if (right_var)
        {
            right = p1->second->get_type();
            if (left == 1)
            {// left hand side is a boolean value
                if (right != 1)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    // add a link in variable to its type
                    ((variable *) operands[1])->set_var_type(p1->second);
                    return true;
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else if (left == 2)
            {// left hand side is an integer
                if (right != 2)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                /*int vs = ((int_value *)operands[0])->get_value();
                 if(((rangedint *)(p1->second))->is_valid_value(vs)) {// the value is in the correct range
                 // add a link in variable to its type
                 ((variable *)operands[1])->set_var_type(p1->second);
                 return true;
                 } else {
                 cout << "        " << vs << " is out of bound in " << to_string() << "." << endl;
                 return false;
                 }*/
                ((variable *) operands[1])->set_var_type(p1->second);
                return true;
            }
            else if (left == 3)
            {// left hand side is an enumerate value. It cannot happen. But we still check it.
                //cout<< "        enumerate value cannot appear here." << endl;
                if (right != 3)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    string vs = ((enum_value *) operands[0])->get_value();
                    set<string> * s2 =
                            ((enumerate *) (p1->second))->get_enumvalue();
                    if (s2->find(vs) != s2->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[1])->set_var_type(p1->second);
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs1
                                << " does not have the value " << vs << endl;
                        return false;
                    }
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else
            {// left hand side is an arithmetic expression
                if (p1->second->get_type() == 2
                        && ((arithmetic_expression *) operands[0])->check_var_and_value(
                                obsvars, vars))
                {
                    // add a link in lhs to its type
                    ((variable *) operands[1])->set_var_type(p1->second);
                    return true;
                }
                else
                {
                    cout << "        " << vs1
                            << "does not have integer type or "
                            << ((arithmetic_expression *) operands[0])->to_string()
                            << " is not a correct arithmetic expression."
                            << endl;
                    return false;
                }
            }
        }
        else
        {
            cout << "        " << vs1 << " must be a variable." << endl;
            return false;
        }
    }
    else if (left >= 5 && left <= 8)
    { // left hand side is an arithmetic expression
        if (right == 2) // rhs is an integer
            return ((arithmetic_expression *) operands[0])->check_var_and_value(
                    obsvars, vars);
        else if (right >= 5 && right <= 8) // rhs is an arithmetic expression
            return ((arithmetic_expression *) operands[0])->check_var_and_value(
                    obsvars, vars)
                    && ((arithmetic_expression *) operands[1])->check_var_and_value(
                            obsvars, vars);
        else
        {
            cout << "        right hand side in " << to_string()
                    << " has a wrong type." << endl;
            return false;
        }
    }
    else if (right >= 5 && right <= 8)
    { //right  hand side is an arithmetic expression
        if (left == 2) // lhs is an integer
            return ((arithmetic_expression *) operands[1])->check_var_and_value(
                    obsvars, vars);
        else
        {
            cout << "        left hand side in " << to_string()
                    << " has a wrong type." << endl;
            return false;
        }
    }

    cout << "        illegal logic expression: " << to_string() << endl;
    return false;
}

bool logic_expression::check_global_consistency(map<string, map<string,
        basictype *> > *vars)
{
    unsigned char left = operands[0]->get_type(); // left hand side
    unsigned char right = operands[1]->get_type(); // right hand side
    bool left_var = true;
    bool right_var = true;

    if (left == 0)
    {// left hand side is a variable, or an enumerate value
        variable* v1 = ((variable *) operands[0]);
        string vs = v1->get_variable_name();
        bool left_defined = true;
        map<string, basictype *>::iterator p;
        if (v1->is_agent_name_null())
            left_var = false;
        else
        {
            string ag_name = v1->get_agent_name();
            map<string, map<string, basictype *> >::iterator gp = vars->find(
                    ag_name);
            if (gp == vars->end())
            {
                cout << "    undefined agent " << ag_name << endl;
                left_defined = false;
            }
            else
            {
                p = gp->second.find(vs);
                if (p == gp->second.end())
                {// the variable is not defined
                    cout << "        variable " << vs
                            << " is not defined in agent " << ag_name << endl;
                    left_defined = false;
                }
            }
        }
        if (right == 0)
        {// right hand side could be a variable or a enumerate value
            variable* v2 = ((variable *) operands[1]);
            string vs1 = v2->get_variable_name();
            bool right_defined = true;
            map<string, basictype *>::iterator p1;
            if (v2->is_agent_name_null())
                right_var = false;
            else
            {
                string ag_name = v2->get_agent_name();
                map<string, map<string, basictype *> >::iterator gp =
                        vars->find(ag_name);
                if (gp == vars->end())
                {
                    cout << "    undefined agent " << ag_name << endl;
                    right_defined = false;
                }
                else
                {
                    p1 = gp->second.find(vs1);
                    if (p1 == gp->second.end())
                    {// the variable is not defined
                        cout << "        variable " << vs1
                                << " is not defined in agent " << ag_name
                                << endl;
                        right_defined = false;
                    }
                }
            }
            if (!left_defined || !right_defined)
                return false;
            if (left_var && right_var)
            {// both sides are variables
                //check if both sides have the same type.
                unsigned char t1 = p->second->get_type(); //lhs' type
                unsigned char t2 = p1->second->get_type(); //rhs' type
                if (t1 == t2)
                { // same type
                    if (t1 == 3)
                    {// enumerate type
                        if (op != 0 && op != 1)
                        {
                            cout
                                    << "        only '=' and '<>' are allowed for enumeration variables."
                                    << endl;
                            return false;
                        }
                        set<string> * s1 =
                                ((enumerate *) (p->second))->get_enumvalue();
                        set<string> * s2 =
                                ((enumerate *) (p1->second))->get_enumvalue();
                        if (s1->size() == s2->size())
                        {// same size
                            bool equal = true;
                            for (set<string>::iterator i = s1->begin(); i
                                    != s1->end(); i++)
                                if (s2->find(*i) == s2->end())
                                {
                                    equal = false;
                                    break;
                                }
                            if (equal)
                            {
                                // add a link in variable to its type
                                ((variable *) operands[0])->set_var_type(
                                        p->second);
                                ((variable *) operands[1])->set_var_type(
                                        p1->second);
                                return true;
                            }
                            else
                            {
                                cout << "        " << vs << " and " << vs1
                                        << " do not have the same enumerate type."
                                        << endl;
                                return false;
                            }
                        }
                        else
                        {
                            cout << "        " << vs << " and " << vs1
                                    << " do not have the same enumerate type."
                                    << endl;
                            return false;
                        }
                    }
                    else
                    {
                        if (t1 == 1 && op != 0 && op != 1)
                        {
                            cout
                                    << "        only '=' and '<>' are allowed for boolean variables."
                                    << endl;
                            return false;
                        }
                        ((variable *) operands[0])->set_var_type(p->second);
                        ((variable *) operands[1])->set_var_type(p1->second);
                        return true;
                    }
                }
                else
                {
                    cout << "        " << vs << " and " << vs1
                            << " have different type." << endl;
                    return false;
                }
            }
            else if (left_var && !right_var)
            {// lhs is a variable and rhs is an enumerate value
                if (op != 0 && op != 1)
                {
                    cout
                            << "        only '=' and '<>' are allowed for enumeration variables."
                            << endl;
                    return false;
                }
                unsigned char t1 = p->second->get_type(); //lhs' type
                if (t1 == 3)
                {// lhs must be enumerate
                    set<string> * s1 =
                            ((enumerate *) (p->second))->get_enumvalue();
                    if (s1->find(vs1) != s1->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[0])->set_var_type(p->second);
                        //change the rhs to be an enumerate value
                        operands[1] = new enum_value(new string(vs1));
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs << " does not have the value "
                                << vs1 << endl;
                        return false;
                    }
                }
                else
                {
                    cout << "        " << vs << " must have an enumerate type."
                            << endl;
                    return false;
                }
            }
            else if (!left_var && right_var)
            {// lhs is an enumerate value and rhs is a variable
                if (op != 0 && op != 1)
                {
                    cout
                            << "        only '=' and '<>' are allowed for enumeration variables."
                            << endl;
                    return false;
                }
                unsigned char t2 = p1->second->get_type(); //rhs' type
                if (t2 == 3)
                {// rhs must be enumerate
                    set<string> * s2 =
                            ((enumerate *) (p1->second))->get_enumvalue();
                    if (s2->find(vs) != s2->end())
                    {//find a matched value in the enumerate type
                        // add a link in rhs to its type
                        ((variable *) operands[1])->set_var_type(p1->second);
                        //change the lhs to be an enumerate value
                        operands[0] = new enum_value(new string(vs));
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs1
                                << " does not have the value " << vs << endl;
                        return false;
                    }
                }
                else
                {
                    cout << "        " << vs1
                            << " must have an enumerate type." << endl;
                    return false;
                }
            }
            else
            {
                cout << "        " << vs << " or " << vs1
                        << " must be a variable." << endl;
                return false;
            }
        }
        else if (left_var)
        {
            if (!left_defined)
                return false;
            left = p->second->get_type();
            if (right == 1)
            {// right hand side is a boolean value
                if (left != 1)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    // add a link in variable to its type
                    ((variable *) operands[0])->set_var_type(p->second);
                    return true;
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else if (right == 2)
            {// right hand side is an integer
                if (left != 2)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not a bounded integer variable." << endl;
                    return false;
                }
                /*int vs1 = ((int_value *)operands[1])->get_value();
                 if(((rangedint *)(p->second))->is_valid_value(vs1)) {// the value is in the correct range
                 // add a link in variable to its type
                 ((variable *)operands[0])->set_var_type(p->second);
                 return true;
                 } else {
                 cout << "        " << vs1 << " is out of bound in " << to_string() << "." << endl;
                 return false;
                 }*/
                ((variable *) operands[0])->set_var_type(p->second);
                return true;
            }
            else if (right == 3)
            {// right hand side is an enumerate value. It cannot happen. But we still check it.
                //cout<< "        Can enumeration value appear here?" << endl;
                if (left != 3)
                {
                    cout << "         " << vs << " in " << to_string()
                            << " is not an enumeration variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    string vs1 = ((enum_value *) operands[1])->get_value();
                    set<string> * s1 =
                            ((enumerate *) (p->second))->get_enumvalue();
                    if (s1->find(vs1) != s1->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[0])->set_var_type(p->second);
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs << " does not have the value "
                                << vs1 << endl;
                        return false;
                    }
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else
            {// right hand side is an arithmetic expression
                if (p->second->get_type() == 2
                        && ((arithmetic_expression *) operands[1])->check_var_and_value(
                                vars))
                {
                    // add a link in lhs to its type
                    ((variable *) operands[0])->set_var_type(p->second);
                    return true;
                }
                else
                {
                    cout << "        " << vs
                            << "does not have integer type or "
                            << ((arithmetic_expression *) operands[1])->to_string()
                            << " is not a correct arithmetic expression."
                            << endl;
                    return false;
                }
            }
        }
        else
        {
            cout << "        " << vs << " must be a variable." << endl;
            return false;
        }
    }
    else if (right == 0)
    {// right hand side is a variable
        variable* v2 = ((variable *) operands[1]);
        string vs1 = ((variable *) operands[1])->get_variable_name();
        map<string, basictype *>::iterator p1;
        if (v2->is_agent_name_null())
            right_var = false;
        else
        {
            string ag_name = v2->get_agent_name();
            map<string, map<string, basictype *> >::iterator gp = vars->find(
                    ag_name);
            if (gp == vars->end())
            {
                cout << "    undefined agent " << ag_name << endl;
                return false;
            }
            p1 = gp->second.find(vs1);
            if (p1 == gp->second.end())
            {// the variable is not defined
                cout << "        variable " << vs1
                        << " is not defined in agent " << ag_name << endl;
                return false;
            }
        }
        if (right_var)
        {
            right = p1->second->get_type();
            if (left == 1)
            {// left hand side is a boolean value
                if (right != 1)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    // add a link in variable to its type
                    ((variable *) operands[1])->set_var_type(p1->second);
                    return true;
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else if (left == 2)
            {// left hand side is an integer
                if (right != 2)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not a Boolean variable." << endl;
                    return false;
                }
                /*int vs = ((int_value *)operands[0])->get_value();
                 if(((rangedint *)(p1->second))->is_valid_value(vs)) {// the value is in the correct range
                 // add a link in variable to its type
                 ((variable *)operands[1])->set_var_type(p1->second);
                 return true;
                 } else {
                 cout << "        " << vs << " is out of bound in " << to_string() << "." << endl;
                 return false;
                 }*/
                ((variable *) operands[1])->set_var_type(p1->second);
                return true;
            }
            else if (left == 3)
            {// left hand side is an enumerate value. It cannot happen. But we still check it.
                if (right != 3)
                {
                    cout << "         " << vs1 << " in " << to_string()
                            << " is not an enumeration variable." << endl;
                    return false;
                }
                //cout<< "        enumerate value cannot appear here." << endl;
                if (op == 0 || op == 1)
                {// only equality is allowed here
                    string vs = ((enum_value *) operands[0])->get_value();
                    set<string> * s2 =
                            ((enumerate *) (p1->second))->get_enumvalue();
                    if (s2->find(vs) != s2->end())
                    {//find a matched value in the enumerate type
                        // add a link in lhs to its type
                        ((variable *) operands[1])->set_var_type(p1->second);
                        return true;
                    }
                    else
                    {
                        cout << "        " << vs1
                                << " does not have the value " << vs << endl;
                        return false;
                    }
                }
                else
                {
                    cout
                            << "        only equality or inequality test is allowed in "
                            << to_string() << "." << endl;
                    return false;
                }
            }
            else
            {// left hand side is an arithmetic expression
                if (p1->second->get_type() == 2
                        && ((arithmetic_expression *) operands[0])->check_var_and_value(
                                vars))
                {
                    // add a link in lhs to its type
                    ((variable *) operands[1])->set_var_type(p1->second);
                    return true;
                }
                else
                {
                    cout << "        " << vs1
                            << "does not have integer type or "
                            << ((arithmetic_expression *) operands[0])->to_string()
                            << " is not a correct arithmetic expression."
                            << endl;
                    return false;
                }
            }
        }
        else
        {
            cout << "        " << vs1 << " must be a variable." << endl;
            return false;
        }
    }
    else if (left >= 5 && left <= 8)
    { // left hand side is an arithmetic expression
        if (right == 2) // rhs is an integer
            return ((arithmetic_expression *) operands[0])->check_var_and_value(
                    vars);
        else if (right >= 5 && right <= 8) // rhs is an arithmetic expression
            return ((arithmetic_expression *) operands[0])->check_var_and_value(
                    vars)
                    && ((arithmetic_expression *) operands[1])->check_var_and_value(
                            vars);
        else
        {
            cout << "        right hand side in " << to_string()
                    << " has a wrong type." << endl;
            return false;
        }
    }
    else if (right >= 5 && right <= 8)
    { //right  hand side is an arithmetic expression
        if (left == 2) // lhs is an integer
            return ((arithmetic_expression *) operands[1])->check_var_and_value(
                    vars);
        else
        {
            cout << "        left hand side in " << to_string()
                    << " has a wrong type." << endl;
            return false;
        }
    }

    cout << "        illegal logic expression: " << to_string() << endl;
    return false;
}

BDD logic_expression::encode_bdd(BDD* base)
{
    int lhstype = operands[0]->get_type();
    int rhstype = operands[1]->get_type();
    BDD tmpbdd = *base;
    BDD tmpbdd1 = bddmgr->bddOne();
    int begin, end, begin1;
    //cout << "    encoding logic expression '" << to_string() << "'. " << endl;

    if (lhstype == 4)
    { // left hand side is an action
        //cout << "encoding logic expression '" << to_string() << "': ";
        laction *la = (laction *) operands[0];
        basic_agent *ba = la->get_agent();
        begin = ba->get_action_index_begin();
        end = ba->get_action_index_end();
        string act_name = ((variable *) operands[1])->get_variable_name();
        map<string, vector<bool>*>::iterator k =
                ba->get_action_indices()->find(act_name);
        vector<bool>* b = (*k).second;
        for (int i = begin; i <= end; i++)
            tmpbdd = tmpbdd * ((*b)[i - begin] ? (*a)[i] : !(*a)[i]);
        //tmpbdd.print(2, 2);
    }
    else if (lhstype == 0 && rhstype == 0)
    { // two variables
        basictype *var_type = ((variable *) operands[0])->get_var_type();
        basictype *var_type1 = ((variable *) operands[1])->get_var_type();
        if (var_type->get_type() != var_type1->get_type())
        {
            cout << "Error: only two variables in both sides of "
                    << to_string() << " have different types" << endl;
            exit(0);
        }
        begin = var_type->get_index_begin();
        begin1 = var_type1->get_index_begin();
        if (var_type->get_type() == 1)
        { // bool
            if (op != 0 && op != 1)
            {
                cout << "Error: only EQ and NEQ on bool types are allowed in "
                        << to_string() << endl;
                exit(0);
            }
            tmpbdd1 *= ((!(*v)[begin] + (*v)[begin1]) * ((*v)[begin]
                    + !(*v)[begin1]));
            if (op == 1)
                tmpbdd *= !tmpbdd1;
            else
                tmpbdd *= tmpbdd1;
        }
        else if (var_type->get_type() == 2)
        { // rangedint
            ADD rhs = ((rangedint *) var_type1)->build_ADD_tree();
            ADD lhs = ((rangedint *) var_type)->build_ADD_tree();
            ADD result;
            if (op == 0)
                result = addEQ(lhs, rhs);
            else if (op == 1)
                result = addNEQ(lhs, rhs);
            else if (op == 2)
                result = addLT(lhs, rhs);
            else if (op == 3)
                result = addLE(lhs, rhs);
            else if (op == 4)
                result = addGT(lhs, rhs);
            else if (op == 5)
                result = addGE(lhs, rhs);
            tmpbdd *= result.BddThreshold(1);
        }
        else
        { // enumerate
            if (op != 0 && op != 1)
            {
                cout
                        << "Error: only EQ and NEQ on enumerate types are allowed in "
                        << to_string() << endl;
                exit(0);
            }
            ADD rhs = ((enumerate *) var_type1)->build_ADD_tree();
            ADD lhs = ((enumerate *) var_type)->build_ADD_tree();
            ADD result = (op == 0) ? addEQ(lhs, rhs) : addNEQ(lhs, rhs);
            tmpbdd *= result.BddThreshold(1);
        }
    }
    else if (lhstype == 1 || rhstype == 1)
    { // bool value
        variable *var = lhstype == 0 ? (variable *) operands[0]
                : (variable *) operands[1];
        bool_value *value = lhstype == 1 ? (bool_value *) operands[0]
                : (bool_value *) operands[1];
        basictype *var_type = var->get_var_type();
        begin = var_type->get_index_begin();
        if (value->get_value())
            tmpbdd1 *= (*v)[begin];
        else
            tmpbdd1 *= !(*v)[begin];
        if (op == 1)
            tmpbdd *= !tmpbdd1;
        else
            tmpbdd *= tmpbdd1;
    }
    else if (lhstype == 3 || rhstype == 3)
    { // enumerate value
        variable *var = lhstype == 0 ? (variable *) operands[0]
                : (variable *) operands[1];
        basictype *var_type = var->get_var_type();
        begin = var_type->get_index_begin();
        end = var_type->get_index_end();
        string value = lhstype == 3 ? ((enum_value *) operands[0])->get_value()
                : ((enum_value *) operands[1])->get_value();
        vector<bool>* vb = ((enumerate *) var_type)->get_value_index(value);
        for (int i = end; i >= begin; i--)
            if ((*vb)[i - begin])
                tmpbdd1 *= (*v)[i];
            else
                tmpbdd1 *= !(*v)[i];
        if (op == 1)
            tmpbdd *= !tmpbdd1;
        else
            tmpbdd *= tmpbdd1;
    }
    else
    { // arithmetic expression
        ADD
                lhs =
                        lhstype == 0 ? ((variable *) operands[0])->build_ADD_tree()
                                : (lhstype == 2 ? bddmgr->constant(
                                        ((int_value *) operands[0])->get_value())
                                        : ((arithmetic_expression *) operands[0])->build_ADD_tree());
        ADD
                rhs =
                        rhstype == 0 ? ((variable *) operands[1])->build_ADD_tree()
                                : (rhstype == 2 ? bddmgr->constant(
                                        ((int_value *) operands[1])->get_value())
                                        : ((arithmetic_expression *) operands[1])->build_ADD_tree());
        ADD result;
        if (op == 0)
            result = addEQ(lhs, rhs);
        else if (op == 1)
            result = addNEQ(lhs, rhs);
        else if (op == 2)
            result = addLT(lhs, rhs);
        else if (op == 3)
            result = addLE(lhs, rhs);
        else if (op == 4)
            result = addGT(lhs, rhs);
        else if (op == 5)
            result = addGE(lhs, rhs);
        tmpbdd *= result.BddThreshold(1);
    }
    return tmpbdd;
}

/* BDD logic_expression::encode_bdd_negation_protocol(BDDvector* v, BDD base) { // should not be used
 if(op==0) {
 if(operands[0]->get_type()!=0) {
 cout << "error: The left hand side should be a variable!" << endl;
 exit(-1);
 }
 variable *var = (variable *)operands[0];
 basictype *var_type = var->get_var_type();
 unsigned char value_type = var_type->get_type();
 int begin = var_type->get_index_begin();
 int end = var_type->get_index_end();
 BDD tmpbdd = base;

 if(value_type == 1) { // boolean type
 if(((bool_value *)operands[1])->get_value())
 tmpbdd = tmpbdd * !(*v)[begin];
 else
 tmpbdd = tmpbdd * (*v)[begin];
 } else if(value_type == 2) { // rangedint
 bool flag = true;
 int value = ((int_value *)operands[1])->get_value();
 rangedint * r = (rangedint *)var_type;
 for(int k=r->get_lowerbound(); k<=r->get_upperbound(); k++)
 if(k!=value) {
 BDD tmpbdd1 = base;
 vector<int>* vb = r->get_value_index(k);
 for(int i=end; i>=begin; i--)
 if((*vb)[i-begin]==1)
 tmpbdd1 = tmpbdd1 * (*v)[i];
 else if((*vb)[i-begin]==-1)
 tmpbdd1 = tmpbdd1 * !(*v)[i];
 if(flag) {
 tmpbdd = tmpbdd1;
 flag = false;
 } else
 tmpbdd = tmpbdd + tmpbdd1;
 }
 } else { // enumerate
 bool flag = true;
 string value = ((enum_value *)operands[1])->get_value();
 enumerate * e = (enumerate *)var_type;
 set<string> * values = e->get_enumvalue();
 for(set<string>::iterator k=values->begin(); k!=values->end(); k++)
 if(*k!=value) {
 BDD tmpbdd1 = base;
 vector<bool>* vb = e->get_value_index(*k);
 for(int i=end; i>=begin; i--)
 if((*vb)[i-begin])
 tmpbdd1 = tmpbdd1 * (*v)[i];
 else
 tmpbdd1 = tmpbdd1 * !(*v)[i];
 if(flag) {
 tmpbdd = tmpbdd1;
 flag = false;
 } else
 tmpbdd = tmpbdd + tmpbdd1;
 }
 }
 return tmpbdd;
 } else {
 cout << "Currently only equality testing is supported!" << endl;
 exit(-1);
 }
 }*/

logic_expression* logic_expression::permute_agents(
        map<string, string> *permutation)
{
    int lhstype = operands[0]->get_type();
    int rhstype = operands[1]->get_type();

    if (lhstype == 4)
    {
        return new logic_expression(op,
                ((laction *) operands[0])->permute_agents(permutation),
                operands[1]);
    }
    else if (lhstype == 0 && rhstype == 0)
    { // two variables
        return new logic_expression(op,
                ((variable *) operands[0])->permute_agents(permutation),
                ((variable *) operands[1])->permute_agents(permutation));
    }
    else if (lhstype == 1 || rhstype == 1 || lhstype == 3 || rhstype == 3)
    { // bool value or enumerate value
        return lhstype == 0 ? new logic_expression(op,
                ((variable *) operands[0])->permute_agents(permutation),
                operands[1]) : new logic_expression(op, operands[0],
                ((variable *) operands[1])->permute_agents(permutation));
    }
    else
    { // arithmetic expression
        expression
                *lexpr =
                        lhstype == 0 ? ((variable *) operands[0])->permute_agents(
                                permutation)
                                : (lhstype == 2 ? operands[0]
                                        : ((arithmetic_expression *) operands[0])->permute_agents(
                                                permutation));
        expression
                *rexpr =
                        rhstype == 0 ? ((variable *) operands[1])->permute_agents(
                                permutation)
                                : (lhstype == 2 ? operands[1]
                                        : ((arithmetic_expression *) operands[1])->permute_agents(
                                                permutation));
        return new logic_expression(op, lexpr, rexpr);
    }
    return this;
}

bool_expression::bool_expression()
{
    op = 4; // encode "other" branch in protocol
}
bool_expression::bool_expression(unsigned char o, Object *obj1)
{ // single operand
    op = o;
    operands[0] = obj1;
}
bool_expression::bool_expression(unsigned char o, Object *obj1, Object *obj2)
{ // two operands
    op = o;
    operands[0] = obj1;
    operands[1] = obj2;
}
bool_expression::~bool_expression()
{
    cout << "deleting bool_expression " << to_string() << endl;
    //delete []operands;
}
unsigned char bool_expression::get_op()
{
    return op;
}
bool bool_expression::is_other_branch()
{
    if (op == 4)
        return true;
    else
        return false;
}
Object* bool_expression::get_operand(unsigned char i)
{
    if (i > 1 || (i == 1 && (op == 0 || op == 3)))
    {
        cout << "error: bool operand " << i << " does not exist!" << endl;
        exit(1);
    }
    else if (operands[i] == NULL)
    {
        cout << "error: bool operand " << i << " is undefined!" << endl;
        exit(1);
    }
    else
        return (operands[i]);
}
bool bool_expression::equal_to(bool_expression *expr)
{
    if (op == expr->get_op())
        switch (op)
        {
            case 0:
                return ((logic_expression *) (operands[0]))->equal_to(
                        (logic_expression *) expr->get_operand(0));
            case 1:
            case 2:
                return ((bool_expression *) (operands[0]))->equal_to(
                        (bool_expression *) expr->get_operand(0))
                        && ((bool_expression *) (operands[1]))->equal_to(
                                (bool_expression *) expr->get_operand(1));
            case 3:
                return ((bool_expression *) (operands[0]))->equal_to(
                        (bool_expression *) expr->get_operand(0));
            case 4:
            case 5:
                return true;
        }

    return false;
}

string bool_expression::to_string()
{
    if (op == 0)
        return ((logic_expression *) (operands[0]))->to_string();
    else if (op == 1)
        return ((bool_expression *) (operands[0]))->to_string() + " and "
                + ((bool_expression *) (operands[1]))->to_string();
    else if (op == 2)
        return ((bool_expression *) (operands[0]))->to_string() + " or "
                + ((bool_expression *) (operands[1]))->to_string();
    else if (op == 3)
        return "! " + ((bool_expression *) (operands[0]))->to_string();
    else if (op == 4)
        return "Other";
    else if (op == 5)
        return "TRUE";
    else if (op == 6)
        return "FALSE";
    return "error: should not happen.";
}
bool bool_expression::check_var_and_value(map<string, basictype *> *obsvars,
        map<string, basictype *> *vars, string agent_name, map<string,
                basic_agent*> *global_actions)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions)/*check_var_and_value(vars)*/;
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_var_and_value(obsvars,
                vars, agent_name, global_actions);
    else if (op == 1 || op == 2)
    {
        bool b1 = ((bool_expression *) operands[0])->check_var_and_value(
                obsvars, vars, agent_name, global_actions);
        bool b2 = ((bool_expression *) operands[1])->check_var_and_value(
                obsvars, vars, agent_name, global_actions);
        return (b1 && b2);
    }
    else if (op == 4)
        return true;
    else
        return false;
}

bool bool_expression::check_var_and_value_flat(
        map<string, basictype *> *obsvars, map<string, basictype *> *vars,
        string agent_name, map<string, basic_agent*> *global_actions)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions)/*check_var_and_value(vars)*/;
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_var_and_value_flat(
                obsvars, vars, agent_name, global_actions);
    else if (op == 1 || op == 2)
    {
        vector<bool_expression *> *expr_vector =
                new vector<bool_expression *> ();
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, op);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, op);
        bool result = true;
        for (unsigned int i = 0; i < expr_vector->size(); i++)
        {
            result = result && (*expr_vector)[i]->check_var_and_value_flat(
                    obsvars, vars, agent_name, global_actions);
        }
        return result;
    }
    else if (op == 4)
        return true;
    else
        return false;
}

bool bool_expression::check_evolution(map<string, basictype *> *obsvars, map<
        string, basictype *> *vars, string agent_name,
        map<string, basic_agent*> *global_actions)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions);
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions);
    else if (op == 1 || op == 2)
    {
        bool b1 = ((bool_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions);
        bool b2 = ((bool_expression *) operands[1])->check_evolution(obsvars,
                vars, agent_name, global_actions);
        return (b1 && b2);
    }
    else
        return false;
}

bool bool_expression::check_evolution_flat(map<string, basictype *> *obsvars,
        map<string, basictype *> *vars, string agent_name, map<string,
                basic_agent*> *global_actions)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_evolution(obsvars,
                vars, agent_name, global_actions);
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_evolution_flat(obsvars,
                vars, agent_name, global_actions);
    else if (op == 1 || op == 2)
    {
        vector<bool_expression *> *expr_vector =
                new vector<bool_expression *> ();
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, op);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, op);
        bool result = true;
        for (unsigned int i = 0; i < expr_vector->size(); i++)
        {
            result = result && (*expr_vector)[i]->check_evolution_flat(obsvars,
                    vars, agent_name, global_actions);
        }
        return result;
    }
    else
        return false;
}

bool bool_expression::check_global_consistency(map<string, map<string,
        basictype *> > *vars)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_global_consistency(
                vars);
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_global_consistency(vars);
    else if (op == 1 || op == 2)
    {
        bool b1 = ((bool_expression *) operands[0])->check_global_consistency(
                vars);
        bool b2 = ((bool_expression *) operands[1])->check_global_consistency(
                vars);
        return (b1 && b2);
    }
    else
        return false;
}

bool bool_expression::check_global_consistency_flat(map<string, map<string,
        basictype *> > *vars)
{
    if (op == 0) // logic_expression
        return ((logic_expression *) operands[0])->check_global_consistency(
                vars);
    else if (op == 3) // not operaror
        return ((bool_expression *) operands[0])->check_global_consistency_flat(
                vars);
    else if (op == 1 || op == 2)
    {
        vector<bool_expression *> *expr_vector =
                new vector<bool_expression *> ();
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, op);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, op);
        bool result = true;
        for (unsigned int i = 0; i < expr_vector->size(); i++)
        {
            result = result
                    && (*expr_vector)[i]->check_global_consistency_flat(vars);
        }
        return result;
    }
    else
        return false;
}

/*bool_expression bool_expression::negation_down() {
 if(op==0) {// logic_expression
 bool_expression b(3, this);
 return b;
 }
 else if(op==3) // not operaror
 return ((bool_expression *)operands[0])->push_negation_inside();
 else if(op==1) { // and
 bool_expression b1 = ((bool_expression *)operands[0])->negation_down();
 bool_expression b2 = ((bool_expression *)operands[1])->negation_down();
 bool_expression b(2, &b1, &b2);
 return b;
 } else { // or
 bool_expression b1 = ((bool_expression *)operands[0])->negation_down();
 bool_expression b2 = ((bool_expression *)operands[1])->negation_down();
 bool_expression b(1, &b1, &b2);
 return b;
 }
 }

 bool_expression bool_expression::push_negation_inside() {
 if(op==0) // logic_expression
 return *this;
 else if(op==3) // not operaror
 return ((bool_expression *)operands[0])->negation_down();
 else { // and , or
 bool_expression b1 = ((bool_expression *)operands[0])->push_negation_inside();
 bool_expression b2 = ((bool_expression *)operands[1])->push_negation_inside();
 bool_expression b(op, &b1, &b2);
 return b;
 }
 }*/

BDD bool_expression::encode_bdd(BDD* base)
{
    if (options["debug"] == 1)
    {
        cout << "DEBUG:" << endl;
        cout << "    Now encoding " << this->to_string() << endl;
        cout << "DEBUG end" << endl;
    }
    if (op == 0)
    {// logic_expression
        return ((logic_expression *) operands[0])->encode_bdd(base);
    }
    else if (op == 3)
    {// not operaror
        return !((bool_expression *) operands[0])->encode_bdd(base);
    }
    else if (op == 1)
    { // and operaror
        BDD b1 = ((bool_expression *) operands[0])->encode_bdd(base);
        BDD b2 = ((bool_expression *) operands[1])->encode_bdd(base);
        return b1 * b2;
    }
    else if (op == 2)
    { // or operaror
        BDD b1 = ((bool_expression *) operands[0])->encode_bdd(base);
        BDD b2 = ((bool_expression *) operands[1])->encode_bdd(base);
        return b1 + b2;
    }
    else if (op == 5)
    { // true
        return bddmgr->bddOne();
    }
    else if (op == 6)
    { // false
        return bddmgr->bddZero();
    }
    else
    {
        return *base;
    }
}

void bool_expression::collect_exprs(vector<bool_expression *> *expr_vector,
        unsigned int type)
{
    if (op == type)
    {
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, type);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, type);
    }
    else
        expr_vector->push_back(this);
}

BDD bool_expression::encode_bdd_flat(BDD* base)
{
    if (op == 0)
    {// logic_expression
        return ((logic_expression *) operands[0])->encode_bdd(base);
    }
    else if (op == 3)
    {// not operaror
        return !((bool_expression *) operands[0])->encode_bdd_flat(base);
    }
    else if (op == 1)
    { // and operaror
        vector<bool_expression *> *expr_vector =
                new vector<bool_expression *> ();
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, op);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, op);
        BDD result = bddmgr->bddOne();
        for (unsigned int i = 0; i < expr_vector->size(); i++)
        {
            result = result * (*expr_vector)[i]->encode_bdd_flat(base);
        }
        return result;
    }
    else if (op == 2)
    { // or operaror
        vector<bool_expression *> *expr_vector =
                new vector<bool_expression *> ();
        ((bool_expression *) operands[0])->collect_exprs(expr_vector, op);
        ((bool_expression *) operands[1])->collect_exprs(expr_vector, op);
        BDD result = bddmgr->bddZero();
        for (unsigned int i = 0; i < expr_vector->size(); i++)
        {
            result = result + (*expr_vector)[i]->encode_bdd_flat(base);
        }
        return result;
    }
    else if (op == 5)
    { // true
        return bddmgr->bddOne();
    }
    else if (op == 6)
    { // false
        return bddmgr->bddZero();
    }
    else
    {
        return *base;
    }
}

bool_expression* bool_expression::permute_agents(
        map<string, string> *permutation)
{
    switch (op)
    {
        case 0: // logic_expression
            return new bool_expression(0,
                    ((logic_expression *) operands[0])->permute_agents(
                            permutation));
        case 3: // not operaror
            return new bool_expression(3,
                    ((bool_expression *) operands[0])->permute_agents(
                            permutation));
        case 1: // and operaror
        {
            bool_expression *b1 =
                    ((bool_expression *) operands[0])->permute_agents(
                            permutation);
            bool_expression *b2 =
                    ((bool_expression *) operands[1])->permute_agents(
                            permutation);
            return new bool_expression(1, b1, b2);
        }
        case 2: // or operaror
        {
            bool_expression *b1 =
                    ((bool_expression *) operands[0])->permute_agents(
                            permutation);
            bool_expression *b2 =
                    ((bool_expression *) operands[1])->permute_agents(
                            permutation);
            return new bool_expression(2, b1, b2);
        }
    }
    return this;
}

fairness_expression::fairness_expression(unsigned char o, modal_formula *f1,
        modal_formula *f2, modal_formula *f3) :
    modal_formula(o, f1, f2, f3)
{
    //bdd_representation =  fairset;
}

fairness_expression::fairness_expression(unsigned char o, modal_formula *f1,
        modal_formula *f2) :
    modal_formula(o, f1, f2)
{
    //bdd_representation =  fairset;
}

fairness_expression::fairness_expression(unsigned char o, modal_formula *f1) :
    modal_formula(o, f1)
{
    //bdd_representation =  fairset;
}

fairness_expression::fairness_expression(atomic_proposition *obj1) :
    modal_formula(obj1)
{
    //bdd_representation =  fairset;
}

BDD fairness_expression::get_bdd_representation()
{
    return bdd_representation;
}

void fairness_expression::set_bdd_representation(BDD bddrep)
{
    bdd_representation = bddrep;
}

atomic_proposition::atomic_proposition(string *t)
{
    proposition = t;
}
atomic_proposition::~atomic_proposition()
{
    cout << "deleting atomic_proposition " << to_string() << endl;
    //delete proposition;
}
string atomic_proposition::get_proposition()
{
    if (proposition == NULL)
    {
        cout << "atomic proposition is unknown!" << endl;
        exit(1);
    }
    else
        return *proposition;
}
string atomic_proposition::to_string()
{
    return get_proposition();
}

modal_formula::modal_formula(atomic_proposition *obj1)
{ // term
    op = 0;
    obj[0] = obj1;
}

modal_formula::modal_formula(unsigned char o, modal_formula *f1)
{ // sigle operand formula
    op = o;
    obj[0] = f1;
}

modal_formula::modal_formula(unsigned char o, modal_formula *f1,
        modal_formula *f2)
{ // two operands formula
    op = o;
    obj[0] = f1;
    obj[1] = f2;
}

modal_formula::modal_formula(unsigned char o, modal_formula *f1,
        modal_formula *f2, modal_formula *f3)
{ // three operands formula
    op = o;
    obj[0] = f1;
    obj[1] = f2;
    obj[2] = f3;
}
modal_formula::~modal_formula()
{
    if (options["verbosity"] > 9)
    {
        cout << "deleting modal_formula " << to_string() << endl;
        //delete []obj;
    }
}

unsigned char modal_formula::get_op()
{
    return op;
}

Object* modal_formula::get_operand(unsigned char i)
{
    if (i == 0 && obj[0] != NULL)
        return (obj[0]);
    else if (i == 1 && obj[1] != NULL && (op == 1 || op == 2 || op == 4 || op
            == 16 || op == 17 || op == 30 || op == 31 || op == 32 || op == 40
            || op == 41 || op == 42 || op == 43 || op == 45 || op == 46 || op
            == 47 || op == 48 || op == 50))
    {
        return (obj[1]);
    }
    else if (i == 2 && obj[2] != NULL && (op == 41 || op == 43 || op == 48))
        return (obj[2]);
    else
    {
        cout << " error: operand " << i << " not found!" << endl;
        exit(1);
    }
}
string modal_formula::to_string()
{
    if (op == 0)
        return ((atomic_proposition *) obj[0])->to_string();
    else if (op == 1)
        return "(" + ((modal_formula *) obj[0])->to_string() + " && "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 2)
        return "(" + ((modal_formula *) obj[0])->to_string() + " || "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 3)
        return "(! " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 4)
        return "(" + ((modal_formula *) obj[0])->to_string() + " -> "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 10)
        return "(AG " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 11)
        return "(EG " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 12)
        return "(AX " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 13)
        return "(EX " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 14)
        return "(AF " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 15)
        return "(EF " + ((modal_formula *) obj[0])->to_string() + ")";
    else if (op == 16)
        return "A(" + ((modal_formula *) obj[0])->to_string() + " U "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 17)
        return "E(" + ((modal_formula *) obj[0])->to_string() + " U "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 30)
        return "K(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 31)
        return "GK(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 32)
        return "GCK(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 40)
        return "O(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 41)
        return "KH(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ", "
                + ((modal_formula *) obj[2])->to_string() + ")";
    else if (op == 42)
        return "DK(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 43)
        return "DKH(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ", "
                + ((modal_formula *) obj[2])->to_string() + ")";
    else if (op == 45)
        return "(<" + ((modal_formula *) obj[0])->to_string() + ">X "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 46)
        return "(<" + ((modal_formula *) obj[0])->to_string() + ">F "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 47)
        return "(<" + ((modal_formula *) obj[0])->to_string() + ">G "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else if (op == 50)
        return "KB(" + ((modal_formula *) obj[0])->to_string() + ", "
                + ((modal_formula *) obj[1])->to_string() + ")";
    else
        return "<" + ((modal_formula *) obj[0])->to_string() + ">("
                + ((modal_formula *) obj[1])->to_string() + " U "
                + ((modal_formula *) obj[2])->to_string() + ")";
}

bool modal_formula::check_atomic_proposition(unsigned char type)
{
    // type=0: atomic proposition, type=1: agent, type=2: group, type=3: agent or group
    bool b1, b2, b3;
    switch (op)
    {
        case 1: // AND
        case 2: // OR
        case 4: // IMPLIES
        case 16: // AU
        case 17: // EU
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(0);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(0);
            return (b1 && b2);
        case 3: // NOT
        case 10: // AG
        case 11: // EG
        case 12: // AX
        case 13: // EX
        case 14: // AF
        case 15: // EF
            return ((modal_formula *) obj[0])->check_atomic_proposition(0);
        case 30: // K
        case 50: // KB
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(1);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(0);
            return (b1 && b2);
        case 40: // O -- Does it allow a group name to appear?
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(1);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(0);
            /*if(b1) {
             string name = ((atomic_proposition *)(((modal_formula *)obj[0])->get_operand(0)))->get_proposition();
             bool_expression *ag_red = (*is_agents)[name]->get_redstates();
             if(ag_red==NULL) {
             cout << "    agent " << name << " does not have any red states." << endl;
             return false;
             }
             }*/
            return (b1 && b2);
        case 31: // GK
        case 32: // GCK
        case 42: // DK
        case 45: // ATL X
        case 46: // ATL F
        case 47: // ATL G
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(2);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(0);
            return (b1 && b2);
        case 41: // KH
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(1);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(3);
            b3 = ((modal_formula *) obj[2])->check_atomic_proposition(0);
            return (b1 && b2 && b3);
        case 43: // DKH
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(2);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(3);
            b3 = ((modal_formula *) obj[2])->check_atomic_proposition(0);
            return (b1 && b2 && b3);
        case 48: // ATL U
            b1 = ((modal_formula *) obj[0])->check_atomic_proposition(2);
            b2 = ((modal_formula *) obj[1])->check_atomic_proposition(0);
            b3 = ((modal_formula *) obj[2])->check_atomic_proposition(0);
            return (b1 && b2 && b3);
        case 0: // A leaf node
            string name = ((atomic_proposition *) obj[0])->get_proposition();
            switch (type)
            {
                case 0:
                    if (is_evaluation->find(name) == is_evaluation->end())
                    {
                        cout << "    atomic proposition " << name
                                << " is not defined." << endl;
                        return false;
                    }
                    else
                        return true;
                case 1:
                    if (is_agents->find(name) == is_agents->end())
                    {
                        cout << "    agent " << name << " is not defined."
                                << endl;
                        return false;
                    }
                    else
                        return true;
                case 2:
                    if (is_groups->find(name) == is_groups->end())
                    {
                        cout << "    group " << name << " is not defined."
                                << endl;
                        return false;
                    }
                    else
                        return true;
                case 3:
                    if (is_agents->find(name) == is_agents->end()
                            && is_groups->find(name) == is_groups->end())
                    {
                        cout << "    agent " << name << " is not defined."
                                << endl;
                        return false;
                    }
                    else
                        return true;
            }
    }
    return false;
}
void modal_formula::look_flags(bool *epistemic, bool *deontic,
        bool *common_knowledge, bool *deontic_knowledge,
        bool *distributed_knowledge)
{
    string name;
    Object* id;
    switch (op)
    {
        case 1: // AND
        case 2: // OR
        case 4: // IMPLIES
        case 16: // AU
        case 17: // EU
            ((modal_formula *) obj[0])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 3: // NOT
        case 10: // AG
        case 11: // EG
        case 12: // AX
        case 13: // EX
        case 14: // AF
        case 15: // EF
            ((modal_formula *) obj[0])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 30: // K
        case 50: // KB
            *epistemic = true;
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 40: // O -- Does it allow a group name to appear?
            *deontic = true;
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 31: // GK
            *epistemic = true;
            *common_knowledge = true;
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 32: // GCK
            *epistemic = true;
            *common_knowledge = true;
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 42: // DK
            *epistemic = true;
            *distributed_knowledge = true;
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 45: // ATL X
        case 46: // ATL F
        case 47: // ATL G
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 41: // KH
            *deontic = true;
            *epistemic = true;
            id = ((modal_formula *) obj[1])->get_operand(1);
            name = ((atomic_proposition *) id)->get_proposition();
            if (is_groups->find(name) != is_groups->end()) // the second parameter is a group
                *deontic_knowledge = true;
            ((modal_formula *) obj[2])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 43: // DKH
            *deontic = true;
            *epistemic = true;
            *distributed_knowledge = true;
            id = ((modal_formula *) obj[1])->get_operand(1);
            name = ((atomic_proposition *) id)->get_proposition();
            if (is_groups->find(name) != is_groups->end()) // the second parameter is a group
                *deontic_knowledge = true;
            ((modal_formula *) obj[2])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 48: // ATL U
            ((modal_formula *) obj[1])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            ((modal_formula *) obj[2])->look_flags(epistemic, deontic,
                    common_knowledge, deontic_knowledge, distributed_knowledge);
            return;
        case 0: // A leaf node
            return;
    }
}

BDD modal_formula::check_formula()
{
    // Returns a BDD encoding the set of states in which the formula
    // pointed by pnode is true

    BDD result, rel, af;
    string name, name1;
    Object *id, *id1;

    if (options["debug"] == 1)
    {
        cout << "DEBUG: " << endl;
        cout << "    Now checking formula (or subformula):" << endl;
        cout << "      " << this->to_string() << endl;
        cout << "DEBUG end " << endl;
    }

    switch (op)
    {
        case 0: // leaf
        {
            name = ((atomic_proposition *) obj[0])->get_proposition();
            if (name == "_init")
                return in_st;

            //cout << name << endl;

            if (options["bddcache"] == 2 || options["bddcache"] == 3)
                if (symmetry_cache->find(name) != symmetry_cache->end())
                    return ((*symmetry_cache)[name]);

            bool_expression* simple = is_evaluation->find(name)->second;
            result = simple->encode_bdd(bddOne) * reach;

            if (options["bddcache"] == 2 || options["bddcache"] == 3)
                (*symmetry_cache)[name] = result;

            if (options["debug"] == 1)
            {
                cout << "DEBUG: " << endl;
                cout << "     Simple expression: " << simple->to_string()
                        << endl;
                result.print(2, 2);
                cout << "DEBUG end" << endl;
            }
            //result=evaluation->find(name)->second->encode_bdd(v, a, bddmgr->bddOne())*reach;
            break;
        }
        case 1: // AND
            result = ((modal_formula*) obj[0])->check_formula()
                    * ((modal_formula*) obj[1])->check_formula();
            break;
        case 2: // OR
            result = ((modal_formula*) obj[0])->check_formula()
                    + ((modal_formula*) obj[1])->check_formula();
            break;
        case 3: // NOT
            result = !((modal_formula*) obj[0])->check_formula() * reach;
            break;
        case 4: // IMPLIES
        {
            BDD res1 = !(((modal_formula*) obj[0])->check_formula());

            if (options["debug"] == 1)
            {
                cout << "DEBUG IMPLICATION: " << endl;
                cout << "res1" << endl;
                res1.print(2, 2);
                cout << "DEBUG end" << endl;
            }

            BDD res2 = (((modal_formula*) obj[1])->check_formula() * reach);

            if (options["debug"] == 1)
            {
                cout << "DEBUG: " << endl;
                cout << "res2" << endl;
                res2.print(2, 2);
                cout << "DEBUG end" << endl;
            }

            result = res1 * reach + res2;

            if (options["debug"] == 1)
            {
                cout << "DEBUG: " << endl;
                cout << "result" << endl;
                result.print(2, 2);
                cout << "DEBUG end" << endl;
            }

            /*
             result = (!((modal_formula*)obj[0])->check_formula()*reach +
             ((modal_formula*)obj[1])->check_formula())*reach;
             */
            //cout << to_string();
            //result.print(2, 2);

            break;
        }
        case 10: // AG p = !EF !p
            result = (!check_EF((!((modal_formula*) obj[0])-> check_formula())
                    * reach)) * reach;
            break;
        case 11: // EG
            result = check_EG(((modal_formula*) obj[0])-> check_formula());
            break;
        case 12: // AX p = ! EX !p
            result = !check_EX(!((modal_formula*) obj[0])-> check_formula())
                    * reach;
            break;
        case 13: // EX
            result = check_EX(((modal_formula*) obj[0])-> check_formula());
            break;
        case 14: // AF p = !EG !p
            result = (!check_EG((!((modal_formula*) obj[0])-> check_formula())
                    * reach)) * reach;
            //cout << to_string() << ": ";
            //result.print(v->count(), 2);
            break;
        case 15: // EF p = p \lor EX EF p
            result = check_EF(((modal_formula*) obj[0])-> check_formula());
            /* cout << to_string();
             result.print(2, 2);

             af = (!check_EG(!((modal_formula*)obj[0])->
             check_formula()*reach))*reach;
             if(result < af)
             cout << "EF is less than AF" << endl;
             else if(result == af)
             cout << "EF is equal to AF" << endl;
             else
             cout << "EF is greater than AF" << endl; */
            break;
        case 16: // AU (see check_AU)
            result = check_AU(((modal_formula*) obj[0])-> check_formula(),
                    ((modal_formula*) obj[1])-> check_formula());
            break;
        case 17: // EU
            result = check_EU(((modal_formula*) obj[0])-> check_formula(),
                    ((modal_formula*) obj[1])-> check_formula());
            break;
        case 30: // K
        {
            /*
             * Name is the agent
             * af is set of reachable states in which the formula *doesnt* hold
             */
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            af = !((modal_formula*) obj[1])->check_formula() * reach;

            /*
             *
             */
            result = reach - get_nK_states(&af, name);
            break;
        }
        case 50: // KB
        {
            id = ((modal_formula*) obj[0])->get_operand(0);

            // Name is the name of agent
            name = ((atomic_proposition *) id)->get_proposition();

            // AF is set of reachable states in which the formula holds
            af = ((modal_formula*) obj[1])->check_formula() * reach;

            // result is the reachable states which are indistinguishable for agent name
            result = get_nK_states(&af, name) * reach;
            break;
        }
        case 31: // Everybody knows
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_GK(((modal_formula*) obj[1])-> check_formula(),
                    gm[name]);
            //      result.print(2,2);
            break;
        case 32: // Common knowledge
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            if (options["lazyGCK"] == 0)
                result = check_GCK(((modal_formula*) obj[1])-> check_formula(),
                        gm[name]) * reach;
            else
            {
                result = check_GCK_new(
                        ((modal_formula*) obj[1])-> check_formula(), name)
                        * reach;
            }
            break;
        case 40: // O
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = !check_nO(!((modal_formula*) obj[1])-> check_formula()
                    * reach, deor[name]) * reach;
            break;
        case 41: // KH
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            id1 = ((modal_formula*) obj[1])->get_operand(0);
            name1 = ((atomic_proposition *) id1)->get_proposition();
            if (is_agents->find(name1) != is_agents->end())
                rel = deor[name1];
            else
                rel = deogm[name1];
            result = !check_nKH(!((modal_formula*) obj[2])-> check_formula()
                    * reach, er[name], rel) * reach;
            break;
        case 42: // Distributed knowledge
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_DK(((modal_formula*) obj[1])-> check_formula(),
                    distgm[name]);
            break;
        case 43: // Distributed knowledge assuming
            // correct behaviour
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            id1 = ((modal_formula*) obj[1])->get_operand(0);
            name1 = ((atomic_proposition *) id1)->get_proposition();
            if (is_agents->find(name1) != is_agents->end())
                rel = deor[name1];
            else
                rel = deogm[name1];
            result = !check_nDKH(!((modal_formula*) obj[2])-> check_formula()
                    * reach, distgm[name], rel) * reach;
            break;
        case 45: // ATL operator X
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_ATLX(((modal_formula*) obj[1])-> check_formula(),
                    name);
            break;
        case 46: // ATL operator F
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_ATLU(bddmgr->bddOne(),
                    ((modal_formula*) obj[1])-> check_formula(), name);
            break;
        case 47: // ATL operator G
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_ATLG(((modal_formula*) obj[1])-> check_formula(),
                    name);
            break;
        case 48: // ATL operator U
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_ATLU(((modal_formula*) obj[1])-> check_formula(),
                    ((modal_formula*) obj[2])-> check_formula(), name);
            break;
    }
    return result * reach;
}

BDD modal_formula::check_formula_symmetry(
        vector<map<string, string>*>* permutations)
{
    // Symmetry reduction
    // Returns a BDD encoding the set of states in which the formula
    // pointed by pnode is true

    BDD result, af;
    string name, name1;
    Object *id;

    switch (op)
    {
        case 0: // leaf
        {
            //cout << "in modal_formula::check_formula_symmetry: ";
            //cout.flush();
            name = ((atomic_proposition *) obj[0])->get_proposition();

            if (symmetry_cache->find(name) != symmetry_cache->end())
                return ((*symmetry_cache)[name]);

            /*if(name.compare("_init")==0) {
             return in_st;
             }*/

            //cout << name << endl;
            bool_expression* simple = is_evaluation->find(name)->second;
            //cout << simple->to_string() << endl;
            result = simple->encode_bdd(bddOne) * reach;

            (*symmetry_cache)[name] = result;
            break;
        }
        case 1: // AND
            result = ((modal_formula*) obj[0])->check_formula_symmetry(
                    permutations)
                    * ((modal_formula*) obj[1])->check_formula_symmetry(
                            permutations);
            break;
        case 2: // OR
            result = ((modal_formula*) obj[0])->check_formula_symmetry(
                    permutations)
                    + ((modal_formula*) obj[1])->check_formula_symmetry(
                            permutations);
            break;
        case 3: // NOT
            result = !((modal_formula*) obj[0])->check_formula_symmetry(
                    permutations) * reach;
            break;
        case 4: // IMPLIES
        {
            BDD res1 = !(((modal_formula*) obj[0])->check_formula_symmetry(
                    permutations));

            BDD res2 = (((modal_formula*) obj[1])->check_formula_symmetry(
                    permutations) * reach);

            result = res1 * reach + res2;
            break;
        }
        case 10:
        {// AG p = !EF !p
            if (options["symmetry"] > 2)
            {
                name = to_string();
                if (symmetry_cache->find(name) != symmetry_cache->end())
                {
                    //cout << "found a BDD for " << name << endl;
                    return ((*symmetry_cache)[name]);
                }
            }
            result = (!check_EF(
                    (!((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations)) * reach)) * reach;
            if (options["symmetry"] > 2)
                (*symmetry_cache)[name] = result;
            break;
        }
        case 11: // EG
            result = check_EG(
                    ((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations));
            break;
        case 12: // AX p = ! EX !p
            result = !check_EX(
                    !((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations)) * reach;
            break;
        case 13: // EX
            result = check_EX(
                    ((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations));
            break;
        case 14: // AF p = !EG !p
            result = (!check_EG(
                    (!((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations)) * reach)) * reach;
            //cout << to_string() << ": ";
            //result.print(v->count(), 2);
            break;
        case 15: // EF p = p \lor EX EF p
            result = check_EF(
                    ((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations));
            break;
        case 16: // AU (see check_AU)
            result = check_AU(
                    ((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations),
                    ((modal_formula*) obj[1])-> check_formula_symmetry(
                            permutations));
            break;
        case 17: // EU
            result = check_EU(
                    ((modal_formula*) obj[0])-> check_formula_symmetry(
                            permutations),
                    ((modal_formula*) obj[1])-> check_formula_symmetry(
                            permutations));
            break;
        case 30: // K
        {
            string formula_name = to_string();
            if (symmetry_cache->find(formula_name) != symmetry_cache->end())
            {
                //cout << "found a BDD for " << formula_name << endl;
                return ((*symmetry_cache)[formula_name]);
            }
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            af = bddmgr->bddZero();
            for (long unsigned int i = 0; i < permutations->size(); i++)
            {
                map<string, string>* permutation = (*permutations)[i];
                modal_formula *new_formula =
                        ((modal_formula*) obj[1])->permute_agents(permutation);
                name1 = (*permutation)[name];
                if (options["symmetry"] > 2)
                {
                    string nk_str = "nk-" + name + "-" + name1 + "-"
                            + new_formula->to_string();
                    if (symmetry_cache->find(nk_str) != symmetry_cache->end())
                    {
                        //cout << "    find nk:" << nk_str << endl;
                        af = af + ((*symmetry_cache)[nk_str]);
                    }
                    else
                    {
                        BDD tmp = check_nK(
                                !new_formula->check_formula_symmetry(
                                        permutations) * reach, permuteAgents(
                                        name, name1));
                        (*symmetry_cache)[nk_str] = tmp;
                        af = af + tmp;
                    }
                }
                else
                    af = af + check_nK(!new_formula->check_formula_symmetry(
                            permutations) * reach, permuteAgents(name, name1));
            }
            //time_t t0 = time( 0 );
            //for(int i=0; i<10000; i++)
            //result = !check_nK(af, er[name]) * reach;
            //time_t t1 = time( 0 );
            //for(int i=0; i<10000; i++)
            result = reach - af;
            //time_t t2 = time( 0 );
            //for(int i=0; i<10000; i++)
            //	rel = !get_nK_states(&af, name) * reach;
            //time_t t3 = time( 0 );
            //if(rel!=result) {
            //	cout << "The new algorithm for computing nK is wrong! -- " << to_string() << endl;
            //}
            //else {
            //	cout << "The new algorithm for computing nK is correct! -- " <<
            /*"old: " << difftime(t1, t0) <<*///", new1: " << difftime(t2, t1) << ", new2: " << difftime(t3, t2) << endl;
            //}
            //cout << to_string();
            //result.print(2, 2);
            (*symmetry_cache)[formula_name] = result;
            break;
        }
        case 31: // Everybody knows
        case 32: // Common knowledge
        case 40: // O
        case 41: // KH
        case 42: // Distributed knowledge
        case 43: // Distributed knowledge assuming
        case 45: // ATL operator X
        case 46: // ATL operator F
        case 47: // ATL operator G
        case 48: // ATL operator U
            result = bddmgr->bddZero();
            break;
    }
    return result;
}

BDD modal_formula::check_formula_fair(BDD fair_reach)
{

    // See "Efficient generation of counterexamples and witnesses in
    // symbolic model checking", Clarke Grumberg McMillan Zhao, 1995
    // Section 4, p.3

    // TODO: add all operators

    BDD result, af, rel;
    string name, name1;
    Object *id, *id1;

    if (options["debug"] == 1)
    {
        cout << "DEBUG: " << endl;
        cout << "    Now checking formula (or subformula) under fairness:"
                << endl;
        cout << "      " << this->to_string() << endl;
        cout << "DEBUG end " << endl;
    }

    switch (op)
    {
        case 0: // leaf
        {
            name = ((atomic_proposition *) obj[0])->get_proposition();

            if (options["bddcache"] == 2 || options["bddcache"] == 3)
                if (symmetry_cache->find(name) != symmetry_cache->end())
                    return ((*symmetry_cache)[name]);

            bool_expression* simple = is_evaluation->find(name)->second;
            result = simple->encode_bdd(bddOne) * reach;

            if (options["bddcache"] == 2 || options["bddcache"] == 3)
                (*symmetry_cache)[name] = result;

            if (options["debug"] == 1)
            {
                cout << "DEBUG: " << endl;
                cout << "     Simple expression: " << simple->to_string()
                        << endl;
                result.print(2, 2);
                cout << "DEBUG end" << endl;
            }
            //result=evaluation->find(name)->second->encode_bdd(v, a, bddmgr->bddOne())*reach;
            break;
        }
        case 1: // AND
            result = ((modal_formula*) obj[0])->check_formula_fair(fair_reach)
                    * ((modal_formula*) obj[1])->check_formula_fair(fair_reach);
            break;
        case 2: // OR
            result = ((modal_formula*) obj[0])->check_formula_fair(fair_reach)
                    + ((modal_formula*) obj[1])->check_formula_fair(fair_reach);
            break;
        case 3: // NOT
            result = !((modal_formula*) obj[0])->check_formula_fair(fair_reach)
                    * reach;
            break;
        case 4: // IMPLIES
        {
            BDD res1 = !(((modal_formula*) obj[0])->check_formula_fair(
                    fair_reach));

            BDD res2 = (((modal_formula*) obj[1])->check_formula_fair(
                    fair_reach) * reach);

            result = res1 * reach + res2;

            break;
        }

        case 10: // AG p = !EF !p
            // TODO: check this I'm not 100% sure: the negation of fair path is fair?
            result
                    = (!check_EF_fair(
                            (!((modal_formula*) obj[0])-> check_formula_fair(
                                    fair_reach)) * reach, fair_reach)) * reach;
            //cout << to_string() << ": ";
            //result.print(v->count(), 2);
            break;

        case 11: // EG
        {
            result = check_EG_fair(
                    ((modal_formula*) obj[0])-> check_formula_fair(fair_reach));
            break;
        }
        case 12: // AX p = ! EX !p
            result
                    = !check_EX_fair(
                            !((modal_formula*) obj[0])-> check_formula_fair(
                                    fair_reach), fair_reach) * reach;
            break;
        case 13: // EX
            result = check_EX_fair(
                    ((modal_formula*) obj[0])-> check_formula_fair(fair_reach),
                    fair_reach);
            break;
        case 14: // AF p = !EG !p
            result
                    = !check_EG_fair(
                            !((modal_formula*) obj[0])-> check_formula_fair(
                                    fair_reach)) * reach;
            //cout << to_string() << ": ";
            //result.print(v->count(), 2);
            break;
        case 15: // EF p = p \lor EX EF p
            result = check_EF_fair(
                    ((modal_formula*) obj[0])-> check_formula_fair(fair_reach),
                    fair_reach);
            break;
        case 16: // AU
        {
            BDD p = ((modal_formula*) obj[0])->check_formula_fair(fair_reach);
            BDD q = ((modal_formula*) obj[1])->check_formula_fair(fair_reach);

            result = !(check_EU_fair(!q, !(p + q), fair_reach) + check_EG_fair(
                    !q)) * reach;
            break;
        }
        case 17: // EU
            result = check_EU_fair(
                    ((modal_formula*) obj[0])-> check_formula_fair(fair_reach),
                    ((modal_formula*) obj[1])-> check_formula_fair(fair_reach),
                    fair_reach);
            break;
        case 30: // K
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            /*result = !check_nK_fair(!((modal_formula*)obj[1])->
             check_formula_fair(fair_reach)*reach,
             er[name], fair_reach) * reach;*/
            af = !((modal_formula*) obj[1])->check_formula_fair(fair_reach)
                    * reach;
            result = reach - get_nK_states_fair(&af, name, fair_reach);
            /*if(rel!=result) {
             cout << "The new algorithm for computing nK_fair is wrong! -- " << to_string() << endl;
             }
             else {
             cout << "The new algorithm for computing nK_fair is correct! -- " << endl;
             }*/
            //cout << to_string();
            //result.print(2, 2);
            break;
        case 31: // Everybody knows
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_GK_fair(
                    ((modal_formula*) obj[1])-> check_formula_fair(fair_reach),
                    gm[name], fair_reach);
            //      result.print(2,2);
            break;
        case 32: // Common knowledge
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_GCK_fair(
                    ((modal_formula*) obj[1])-> check_formula_fair(fair_reach),
                    gm[name], fair_reach) * reach;
            break;
        case 40: // O
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = !check_nO_fair(
                    !((modal_formula*) obj[1])-> check_formula_fair(fair_reach)
                            * reach, deor[name], fair_reach) * reach;
            break;
        case 41: // KH
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            id1 = ((modal_formula*) obj[1])->get_operand(0);
            name1 = ((atomic_proposition *) id1)->get_proposition();
            if (is_agents->find(name1) != is_agents->end())
                rel = deor[name1];
            else
                rel = deogm[name1];
            result = !check_nKH_fair(
                    !((modal_formula*) obj[2])-> check_formula_fair(fair_reach)
                            * reach, er[name], rel, fair_reach) * reach;
            break;
        case 42: // Distributed knowledge
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            result = check_DK_fair(
                    ((modal_formula*) obj[1])-> check_formula_fair(fair_reach),
                    distgm[name], fair_reach);
            break;
        case 43: // Distributed knowledge assuming
            // correct behaviour
            id = ((modal_formula*) obj[0])->get_operand(0);
            name = ((atomic_proposition *) id)->get_proposition();
            id1 = ((modal_formula*) obj[1])->get_operand(0);
            name1 = ((atomic_proposition *) id1)->get_proposition();
            if (is_agents->find(name1) != is_agents->end())
                rel = deor[name1];
            else
                rel = deogm[name1];
            result = !check_nDKH_fair(
                    !((modal_formula*) obj[2])-> check_formula_fair(fair_reach)
                            * reach, distgm[name], rel, fair_reach) * reach;
            break;
        default:
            result = check_formula();
            break;
    }

    return result * reach;
}

modal_formula *modal_formula::push_negations_no_k_bar(unsigned int level)
{

    if (options["debug"] == 1)
    {
        cout << "DEBUG: " << endl;
        cout << "    Now in modal_formulapush_negations:" << endl;
        cout << "      " << this->to_string() << endl;
        cout << "      The operator is: " << (int) this->get_op() << endl;
        cout << "DEBUG end " << endl;
    }

    switch (op)
    {
        case 0: // leaf
        {
            //modal_formula *m = new modal_formula((atomic_proposition*)obj[0]);
            //return m;
            return this;
            break;
        }
        case 1: // AND
        case 2: //OR
        {
            modal_formula *m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level),
                    ((modal_formula*) obj[1])->push_negations(level));
            return m;
            break;
        }
        case 3: // NOT
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                // Just copy and return
                //modal_formula * m = new modal_formula(3,(modal_formula*)obj[0]);
                //return m;
                return this;
            }
            else
            {
                // Need to push down negation
                modal_formula *nextformula = (modal_formula*) obj[0];
                unsigned char nextop = nextformula->get_op();

                switch (nextop)
                {
                    case 1: // AND
                    {

                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * result = new modal_formula(2,
                                m1->push_negations(level), m2->push_negations(
                                        level));
                        return result;
                        break;
                    }
                    case 2: // OR
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * result = new modal_formula(1,
                                m1->push_negations(level), m2->push_negations(
                                        level));
                        //cout << "result = " << result->to_string() << endl;
                        return result;
                        break;
                    }
                    case 3: // NOT: negation of negation, remove both.
                    {
                        return ((modal_formula*) nextformula->get_operand(0))->push_negations(
                                level);
                        break;
                    }
                    case 4: // IMPLIES, !(a -> b) = a & !b
                    {
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula
                                * result =
                                        new modal_formula(
                                                1,
                                                ((modal_formula*) nextformula->get_operand(
                                                        0))->push_negations(
                                                        level),
                                                m2->push_negations(level));
                        return result;
                        break;
                    }
                    case 10: // AG: !AG=EF !
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(15,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 11: // EG: !EG=AF!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(14,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 12: // AX
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(13,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 13: // EX
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(12,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 14: // AF : !AF=EG!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(11,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 15: // EF : !EF=AG!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(10,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 16: // AU : a messy one: A[aUb] = ! (E[!bU(!a&!b)] | EG(!b)) (p.216 huth-ryan)
                    {

                        modal_formula * notb = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * nota = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * egnotb = new modal_formula(11, notb);
                        modal_formula * notanotb = new modal_formula(1, nota,
                                notb);
                        modal_formula * until = new modal_formula(17,
                                notb->push_negations(level + 1),
                                notanotb->push_negations(level + 1));
                        modal_formula * result = new modal_formula(2, until,
                                egnotb->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 17: // EU: not sure, see above: E[aUb] = ! (A[!bU(!a&!b)] | AG(!b))
                        // TODO: check this equivalence
                    {
                        modal_formula * notb = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * nota = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * agnotb = new modal_formula(11, notb);
                        modal_formula * notanotb = new modal_formula(1, nota,
                                notb);
                        modal_formula * until = new modal_formula(16,
                                notb->push_negations(level + 1),
                                notanotb->push_negations(level + 1));
                        modal_formula * result = new modal_formula(2, until,
                                agnotb->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 40: // not O_i \phi => EF (g_i and not \phi)
                        if (level == 0)
                        {
                            Object *id =
                                    ((modal_formula*) nextformula->get_operand(
                                            0))->get_operand(0);
                            string
                                    name =
                                            ((atomic_proposition *) id)->get_proposition();
                            string *newap = new string(name + ".GreenStates");
                            //if(is_evaluation->find(*newap) == is_evaluation->end())
                            //  (*is_evaluation)[*newap] = new bool_expression(3, (*is_agents)[name]->get_redstates());
                            modal_formula
                                    *newformula =
                                            new modal_formula(
                                                    3,
                                                    (modal_formula*) nextformula->get_operand(
                                                            1));
                            modal_formula *newformula1 =
                                    newformula->push_negations(1);
                            modal_formula *newformula2 = new modal_formula(
                                    new atomic_proposition(newap));
                            modal_formula *newformula3 = new modal_formula(15,
                                    new modal_formula(1, newformula2,
                                            newformula1));
                            return newformula3;
                        }
                    default:
                    {
                        // Nothing to do for K etc:
                        // Just copy and return
                        //modal_formula * m = new modal_formula(3,(modal_formula*)obj[0]);
                        //return m;
                        return this;
                        break;
                    }
                } // end switch nextop in else:
            } // end else
        } // end case 3 (NOT)
        case 4: // IMPLIES : a->b=!a|b
        {
            modal_formula * m1 = new modal_formula(3, (modal_formula*) obj[0]);
            modal_formula * result = new modal_formula(2, m1->push_negations(
                    level), ((modal_formula*) obj[1])->push_negations(level));
            return result;
            break;
        }
        case 10:
        case 11:
        case 12:
        case 13:
        case 14:
        case 15:
        {
            // Temporal is the first
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level + 1));
            return m;
            break;
        }
        case 16:
        case 17:
        {
            // EU and AU, binary operators:
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level + 1),
                    ((modal_formula*) obj[1])->push_negations(level + 1));
            return m;
            break;
        }
        case 42:
        case 43:
        {
            // KH and DKH are the third thing
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0]), ((modal_formula*) obj[1]),
                    ((modal_formula*) obj[2])->push_negations(level + 1));
            return m;
            break;
        }
        default:
        {
            // Epistemic and deontic is the second
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0]),
                    ((modal_formula*) obj[1])->push_negations(level + 1));
            return m;
            break;
        }
    } // end top case
}

modal_formula *modal_formula::push_negations(unsigned int level)
{
    if (no_kbar)
        return push_negations_no_k_bar(level);

    if (options["debug"] == 1)
    {
        cout << "DEBUG: " << endl;
        cout << "    Now in modal_formulapush_negations:" << endl;
        cout << "      " << this->to_string() << endl;
        cout << "      The operator is: " << (int) this->get_op() << endl;
        cout << "DEBUG end " << endl;
    }

    switch (op)
    {
        case 0: // leaf
        {
            //modal_formula *m = new modal_formula((atomic_proposition*)obj[0]);
            //return m;
            return this;
            break;
        }
        case 1: // AND
        case 2: //OR
        {
            modal_formula *m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level),
                    ((modal_formula*) obj[1])->push_negations(level));
            return m;
            break;
        }
        case 3: // NOT
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                // Just copy and return
                //modal_formula * m = new modal_formula(3,(modal_formula*)obj[0]);
                //return m;
                return this;
            }
            else
            {
                // Need to push down negation
                modal_formula *nextformula = (modal_formula*) obj[0];
                unsigned char nextop = nextformula->get_op();

                switch (nextop)
                {
                    case 1: // AND
                    {

                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * result = new modal_formula(2,
                                m1->push_negations(level), m2->push_negations(
                                        level));
                        return result;
                        break;
                    }
                    case 2: // OR
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * result = new modal_formula(1,
                                m1->push_negations(level), m2->push_negations(
                                        level));
                        //cout << "result = " << result->to_string() << endl;
                        return result;
                        break;
                    }
                    case 3: // NOT: negation of negation, remove both.
                    {
                        return ((modal_formula*) nextformula->get_operand(0))->push_negations(
                                level);
                        break;
                    }
                    case 4: // IMPLIES, !(a -> b) = a & !b
                    {
                        modal_formula * m2 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula
                                * result =
                                        new modal_formula(
                                                1,
                                                ((modal_formula*) nextformula->get_operand(
                                                        0))->push_negations(
                                                        level),
                                                m2->push_negations(level));
                        return result;
                        break;
                    }
                    case 10: // AG: !AG=EF !
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(15,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 30: // K: !K=KB!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));

                        modal_formula * result = new modal_formula(50,
                                (modal_formula*) nextformula->get_operand(0),
                                m1->push_negations(level + 1));

                        return result;
                        break;
                    }
                    case 11: // EG: !EG=AF!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(14,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 12: // AX
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(13,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 13: // EX
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(12,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 14: // AF : !AF=EG!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(11,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 15: // EF : !EF=AG!
                    {
                        modal_formula * m1 = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * result = new modal_formula(10,
                                m1->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 16: // AU : a messy one: A[aUb] = ! (E[!bU(!a&!b)] | EG(!b)) (p.216 huth-ryan)
                    {

                        modal_formula * notb = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * nota = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * egnotb = new modal_formula(11, notb);
                        modal_formula * notanotb = new modal_formula(1, nota,
                                notb);
                        modal_formula * until = new modal_formula(17,
                                notb->push_negations(level + 1),
                                notanotb->push_negations(level + 1));
                        modal_formula * result = new modal_formula(2, until,
                                egnotb->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 17: // EU: not sure, see above: E[aUb] = ! (A[!bU(!a&!b)] | AG(!b))
                        // TODO: check this equivalence
                    {
                        modal_formula * notb = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(1));
                        modal_formula * nota = new modal_formula(3,
                                (modal_formula*) nextformula->get_operand(0));
                        modal_formula * agnotb = new modal_formula(11, notb);
                        modal_formula * notanotb = new modal_formula(1, nota,
                                notb);
                        modal_formula * until = new modal_formula(16,
                                notb->push_negations(level + 1),
                                notanotb->push_negations(level + 1));
                        modal_formula * result = new modal_formula(2, until,
                                agnotb->push_negations(level + 1));
                        return result;
                        break;
                    }
                    case 40: // not O_i \phi => EF (g_i and not \phi)
                        if (level == 0)
                        {
                            Object *id =
                                    ((modal_formula*) nextformula->get_operand(
                                            0))->get_operand(0);
                            string
                                    name =
                                            ((atomic_proposition *) id)->get_proposition();
                            string *newap = new string(name + ".GreenStates");
                            //if(is_evaluation->find(*newap) == is_evaluation->end())
                            //  (*is_evaluation)[*newap] = new bool_expression(3, (*is_agents)[name]->get_redstates());
                            modal_formula
                                    *newformula =
                                            new modal_formula(
                                                    3,
                                                    (modal_formula*) nextformula->get_operand(
                                                            1));
                            modal_formula *newformula1 =
                                    newformula->push_negations(1);
                            modal_formula *newformula2 = new modal_formula(
                                    new atomic_proposition(newap));
                            modal_formula *newformula3 = new modal_formula(15,
                                    new modal_formula(1, newformula2,
                                            newformula1));
                            return newformula3;
                        }
                    default:
                    {
                        // Nothing to do for K etc:
                        // Just copy and return
                        //modal_formula * m = new modal_formula(3,(modal_formula*)obj[0]);
                        //return m;
                        return this;
                        break;
                    }
                } // end switch nextop in else:
            } // end else
        } // end case 3 (NOT)
        case 4: // IMPLIES : a->b=!a|b
        {
            modal_formula * m1 = new modal_formula(3, (modal_formula*) obj[0]);
            modal_formula * result = new modal_formula(2, m1->push_negations(
                    level), ((modal_formula*) obj[1])->push_negations(level));
            return result;
            break;
        }
        case 10:
        case 11:
        case 12:
        case 13:
        case 14:
        case 15:
        {
            // Temporal is the first
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level + 1));
            return m;
            break;
        }
        case 16:
        case 17:
        {
            // EU and AU, binary operators:
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0])->push_negations(level + 1),
                    ((modal_formula*) obj[1])->push_negations(level + 1));
            return m;
            break;
        }
        case 42:
        case 43:
        {
            // KH and DKH are the third thing
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0]), ((modal_formula*) obj[1]),
                    ((modal_formula*) obj[2])->push_negations(level + 1));
            return m;
            break;
        }
        case 30: // K: K a =!KB !a
        {
            // !a
            modal_formula * m1 = new modal_formula(3, (modal_formula*) obj[1]);

            // KB !a
            modal_formula * m2 = new modal_formula(50, (modal_formula*) obj[0],
                    m1->push_negations(level + 1));

            // !KB !a
            modal_formula * result = new modal_formula(3, m2->push_negations(
                    level + 1));

            return result;
            break;
        }
        default:
        {
            // Epistemic and deontic is the second
            modal_formula * m = new modal_formula(op,
                    ((modal_formula*) obj[0]),
                    ((modal_formula*) obj[1])->push_negations(level + 1));
            return m;
            break;
        }
    } // end top case
}

bool modal_formula::is_ACTLK()
{
    /* Return TRUE if the formula is ACTL (i.e., only A quantifiers and
     * K and negation only in front of propositions.
     * All the negations should have been pushed down already.
     */

    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ACTLK()
                    & ((modal_formula*) obj[1])->is_ACTLK());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ACTLK()
                    & ((modal_formula*) obj[1])->is_ACTLK());
            break;
        }
        case 3: // NOT
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return true;
            }
            else
            {
                // however, this case should not be here
                return false;
            }
            break;
        }
        case 4: // IMPLIES
        {
            // Again, this should not be here.
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return ((modal_formula*) obj[1])->is_ACTLK();
            }
            else
            {
                return false;
            }
            break;
        }

        case 10: // AG
        {
            return ((modal_formula*) obj[0])->is_ACTLK();
            break;
        }
        case 11: // EG
        {
            return false;
            break;
        }
        case 12: // AX
        {
            return ((modal_formula*) obj[0])->is_ACTLK();
            break;
        }
        case 13: // EX
        {
            return false;
            break;
        }
        case 14: // AF
        {
            return ((modal_formula*) obj[0])->is_ACTLK();
            break;
        }
        case 15: // EF
        {
            return false;
            break;
        }
        case 16: // AU
        {
            return (((modal_formula*) obj[0])->is_ACTLK()
                    & ((modal_formula*) obj[1])->is_ACTLK());
            break;
        }
        case 17: // EU
        {
            return false;
            break;
        }

            /*case 30: // K
             {
             return ((modal_formula*)obj[1])->is_ACTLK();
             break;
             }
             case 42:
             case 43:
             {	// KH and DKH
             return ((modal_formula*)obj[2])->is_ACTLK();
             break;
             }
             default:
             {
             return ((modal_formula*)obj[1])->is_ACTLK();
             break;
             }*/
        case 30:
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
            return true;
    }

    return false;
}

bool modal_formula::is_ECTLK_BMC()
{
    /*
     * Check if the formula is in ECTL.
     * Negations can only be infront of KB or Atoms
     */

    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ECTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ECTLK_BMC());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ECTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ECTLK_BMC());
            break;
        }
        case 3: // NOT
        {
            return (((modal_formula*) obj[0])->get_op() == 0);
        }
        case 4: // IMPLIES
        {
            // We really shouldn't ever get here ...
            // Implies should have been rewritten by the time we get here

            return false;
        }

        case 10: // AG
        {
            return false;
            break;
        }
        case 11: // EG
        {
            return ((modal_formula*) obj[0])->is_ECTLK_BMC();
            break;
        }
        case 12: // AX
        {
            return false;
            break;
        }
        case 13: // EX
        {
            return ((modal_formula*) obj[0])->is_ECTLK_BMC();
            break;
        }
        case 14: // AF
        {
            return false;
            break;
        }
        case 15: // EF
        {
            return ((modal_formula*) obj[0])->is_ECTLK_BMC();
            break;
        }
        case 16: // AU
        {
            return false;
            break;
        }
        case 17: // EU
        {
            return (((modal_formula*) obj[0])->is_ECTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ECTLK_BMC());
            break;
        }

        case 50: // KB - KB is allowed, K isn't
        {
            return ((modal_formula*) obj[1])->is_ECTLK_BMC();
            break;
        }
    }

    return false;
}

bool modal_formula::atomic_k_bar(modal_formula **atomic_out)
{
    switch (op)
    {
        case 0: // leaf
        {
            return true;
        }
        case 1: // AND
        case 2: // OR
        case 4: // IMPLIES
        case 17: // EU
        {
            return (((modal_formula*) obj[0])->atomic_k_bar(atomic_out) &&
                    ((modal_formula*) obj[1])->atomic_k_bar(atomic_out));
        }
        case 3: // NOT
        case 11: // EG
        case 13: // EX
        case 15: // EF
        {
            return ((modal_formula*) obj[0])->atomic_k_bar(atomic_out);
        }

        case 50: // KB
        {
            (*atomic_out) = ((modal_formula*) obj[1]);
            return ((modal_formula*) obj[1])->is_NoCTLK();
        }
        default:
            return false;
    }
}

bool modal_formula::is_ACTLK_BMC()
{
    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ACTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ACTLK_BMC());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ACTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ACTLK_BMC());
            break;
        }
        case 3: // NOT
        {
            return (((modal_formula*) obj[0])->get_op() == 0);
        }
        case 4: // IMPLIES
        {
            // Implies is ACTL if _both_ halves are ACTLK
            return (((modal_formula*) obj[0])->is_ACTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ACTLK_BMC());
            break;
        }

        case 10: // AG
        {
            return ((modal_formula*) obj[0])->is_ACTLK_BMC();
            break;
        }
        case 11: // EG
        {
            return false;
            break;
        }
        case 12: // AX
        {
            return ((modal_formula*) obj[0])->is_ACTLK_BMC();
            break;
        }
        case 13: // EX
        {
            return false;
            break;
        }
        case 14: // AF
        {
            return ((modal_formula*) obj[0])->is_ACTLK_BMC();
            break;
        }
        case 15: // EF
        {
            return false;
            break;
        }
        case 16: // AU
        {
            return (((modal_formula*) obj[0])->is_ACTLK_BMC()
                    & ((modal_formula*) obj[1])->is_ACTLK_BMC());
            break;
        }
        case 17: // EU
        {
            return false;
            break;
        }

        case 30: // K - K is allowed, KB isn't
        {
            return ((modal_formula*) obj[1])->is_ACTLK_BMC();
            break;
        }
    }

    return false;
}

bool modal_formula::is_ACTLK_new()
{
    /* Return TRUE if the first operator in the formula is ACTL (i.e., only A quantifiers and
     * K and negation only in front of propositions.
     * All the negations should have been pushed down already.
     */

    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ACTLK_new()
                    & ((modal_formula*) obj[1])->is_ACTLK_new());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ACTLK_new()
                    & ((modal_formula*) obj[1])->is_ACTLK_new());
            break;
        }
        case 3: // NOT
        {
            /*if (((modal_formula*)obj[0])->get_op() == 0 ) {
             return true;
             } else {
             // however, this case should not be here
             return false;
             }*/
            return true;
            break;
        }
        case 4: // IMPLIES
        {
            // Again, this should not be here.
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return ((modal_formula*) obj[1])->is_ACTLK_new();
            }
            else
            {
                return false;
            }
            break;
        }

        case 10: // AG
        case 12: // AX
        case 14: // AF
        case 16: // AU
        {
            return true;
        }
        case 11: // EG
        case 13: // EX
        case 15: // EF
        case 17: // EU
        {
            return false;
            break;
        }

        case 30:
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
            return true;
        case 50:
            return false;
    }

    return false;
}

bool modal_formula::is_ECTLK()
{
    /* Return TRUE if the formula is ECTL (i.e., only E quantifiers and
     * \neg K, i.e., negation only in front of propositions and K operator
     */

    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ECTLK()
                    & ((modal_formula*) obj[1])->is_ECTLK());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ECTLK()
                    & ((modal_formula*) obj[1])->is_ECTLK());
            break;
        }
        case 3: // NOT
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return true;
            }
            else if (((modal_formula*) obj[0])->get_op() == 30)
            {
                return ((modal_formula*) (((modal_formula*) obj[0])->get_operand(
                        1)))->is_ECTLK();
                return false;
            }
            else
            {
                return false;
            }
            break;
        }
        case 4: // IMPLIES
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return ((modal_formula*) obj[1])->is_ECTLK();
            }
            else
            {
                return false;
            }
            break;
        }

        case 10: // AG
        {
            return false;
            break;
        }
        case 11: // EG
        {
            return ((modal_formula*) obj[0])->is_ECTLK();
            break;
        }
        case 12: // AX
        {
            return false;
            break;
        }
        case 13: // EX
        {
            return ((modal_formula*) obj[0])->is_ECTLK();
            break;
        }
        case 14: // AF
        {
            return false;
            break;
        }
        case 15: // EF
        {
            return ((modal_formula*) obj[0])->is_ECTLK();
            break;
        }
        case 16: // AU
        {
            return false;
            break;
        }
        case 17: // EU
        {
            return (((modal_formula*) obj[0])->is_ECTLK()
                    & ((modal_formula*) obj[1])->is_ECTLK());
            break;
        }

            /*case 30: // K
             {
             return false;
             break;
             }
             case 42:
             case 43:
             {	// KH and DKH
             return ((modal_formula*)obj[2])->is_ECTLK();
             break;
             }
             default:
             {
             return ((modal_formula*)obj[0])->is_ECTLK();
             break;
             }*/
        case 30:
            return false;
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
        case 50:
            return true;
    }
    return false;
}

bool modal_formula::is_ECTLK_new()
{
    /* Return TRUE if the first operator in the formula is ECTL (i.e., only E quantifiers and
     * \neg K, i.e., negation only in front of propositions and K operator
     */

    switch (op)
    {
        case 0: // leaf
        {
            return true;
            break;
        }
        case 1: // AND
        {
            return (((modal_formula*) obj[0])->is_ECTLK_new()
                    & ((modal_formula*) obj[1])->is_ECTLK_new());
            break;
        }
        case 2: // OR
        {
            return (((modal_formula*) obj[0])->is_ECTLK_new()
                    & ((modal_formula*) obj[1])->is_ECTLK_new());
            break;
        }
        case 3: // NOT
        {
            /*if ( ((modal_formula*)obj[0])->get_op() == 0 ) {
             return true;
             } else if ( ((modal_formula*)obj[0])->get_op() == 30 ) {
             return ((modal_formula*)(((modal_formula*)obj[0])->get_operand(1)))->is_ECTLK_new();
             return false;
             } else {
             return false;
             }*/
            return true;
            break;
        }
        case 4: // IMPLIES
        {
            if (((modal_formula*) obj[0])->get_op() == 0)
            {
                return ((modal_formula*) obj[1])->is_ECTLK_new();
            }
            else
            {
                return false;
            }
            break;
        }

        case 10: // AG
        case 12: // AX
        case 14: // AF
        case 16: // AU
        {
            return false;
        }
        case 11: // EG
        case 13: // EX
        case 15: // EF
        case 17: // EU
        {
            return true;
        }
        case 30:
            return false;
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
        case 50:
            return true;
    }
    return false;
}

/** return true if there is no temporal operator in the formula.
 ** do not check the formula inside epistemic operators */
bool modal_formula::is_NoCTL()
{
    switch (op)
    {
        case 0: // leaf
        case 30:
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
        {
            return true;
        }
        case 1: // AND
        case 2: // OR
        case 4: // IMPLIES
        {
            return (((modal_formula*) obj[0])->is_NoCTL()
                    & ((modal_formula*) obj[1])->is_NoCTL());
        }
        case 3: // NOT
        {
            return ((modal_formula*) obj[0])->is_NoCTL();
        }
    }
    return false;
}

bool modal_formula::is_NoCTLK()
{
    switch (op)
    {
        case 0: // leaf
        {
            return true;
        }
        case 1: // AND
        case 2: // OR
        case 4: // IMPLIES
        {
            return (((modal_formula*) obj[0])->is_NoCTLK()
                    & ((modal_formula*) obj[1])->is_NoCTLK());
        }
        case 3: // NOT
        {
            return ((modal_formula*) obj[0])->is_NoCTLK();
        }
    }
    return false;
}

/* Generate a witness for an ECTLK formula (i.e.  acounterexample
 * for an ACTLK formula), see
 * Clarke et al., "Tree-like counterexamples in model checking"
 * See the algorithm in Figure 7. Essentially, this procedure builds a tree
 * representing a witness for the formula.
 * Returns false if the witness cannot be built (maybe because starting from
 * the wrong initial state)
 */
/** index is used to retrieve the index of the state */
bool modal_formula::build_cex(BDD * state, unsigned int index)
{

    /* TODO: Add fairness */

    vector<BDD *> tmpresult; // a vector to store the states of the witness
    vector<int> desc; // This is a vector of state id (see global variables countex and idbdd)
    vector<transition *> desctr; // This is a vector of transitions (see golbal var cextr)


    if (options["debug"] == 1)
    {
        cout << "DEBUG in build_cex with op = " << (int) op << endl;
    }

    switch (op)
    {
        case 1: // AND
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in AND" << endl;
            }
            bool r2 = ((modal_formula*) obj[1])->build_cex(state, index);
            if (!r2)
                return false;
            bool r1 = ((modal_formula*) obj[0])->build_cex(state, index);
            if (!r1)
                return false;
            return true;
            break;
        }
        case 2: // OR
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in OR" << endl;
            }
            bool r1;
            modal_formula * left = ((modal_formula*) obj[1]);
            BDD * res = new BDD();
            (*res) = left->check_formula();

            if ((*state) <= (*res))
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula " << left->to_string()
                            << " is true in state " << endl;
                }
                r1 = left->build_cex(state, index);
                if (!r1)
                    return false;
            }
            else
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula " << left->to_string()
                            << " is false in state " << endl;
                }
                modal_formula * right = ((modal_formula*) obj[0]);
                r1 = right->build_cex(state, index);
            }
            return r1;
            break;
        }
        case 11: // EG
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in EG" << endl;
            }
            // Need to find a cycle here

            BDD last = check_formula(); // the last state of fixpoint computation

            /* TODO: check fairness here */
            tmpresult.push_back(new BDD(*state));

            vector<BDD *> S; // a vector to store the stages of the computation

            int j = 0;

            BDD Q = bddmgr->bddZero();
            BDD T = bddmgr->bddZero() + *state;

            while (Q == bddmgr->bddZero())
            {

                j++;

                //BDD reachablefromlast = (*(tmpresult[j-1]))*RT;
                BDD reachablefromlast = timesRT(tmpresult[j - 1]);

                reachablefromlast = Exists(v, reachablefromlast);
                reachablefromlast = reachablefromlast.SwapVariables(*v, *pv);

                BDD abdd = reachablefromlast * last;
                if (abdd == bddmgr->bddZero())
                {
                    return false;
                }

                Q = abdd * T; // if this is not false, we found a loop
                if (Q == bddmgr->bddZero())
                {
                    BDD curstate = abdd.PickOneMinterm(*v);

                    tmpresult.push_back(new BDD(curstate));

                    T = T + curstate;
                }
                else
                {
                    break;
                }
            }

            unsigned int numberofstates = (unsigned int) tmpresult.size() - 1; // (the last one is NOT repeated)

            //BDD laststate = (*tmpresult[numberofstates]); // the last one

            int loopstart = -1; // the position where the loop starts

            /*for (int acounter = 0; acounter < numberofstates; acounter++ ) {
             if ( laststate == (*tmpresult[acounter])) {
             loopstart = acounter;
             }
             }*/

            for (unsigned int acounter = 0; acounter <= numberofstates; acounter++)
            {
                if ((Q * (*tmpresult[acounter])) != bddmgr->bddZero())
                {
                    loopstart = acounter;
                    break;
                }
            }

            if (loopstart == -1)
            {
                if (options["quiet"] == 0)
                {
                    cout << "Witness generation for EG:" << endl;
                    cout << "THERE IS A PROBLEM HERE, PLEASE REPORT THIS ERROR"
                            << endl;
                }
                return false;
            }

            // building transitions
            // first go to the last loop state
            //int position = scount;
            int position1 = scount;
            for (unsigned int acounter = 0; acounter < numberofstates; acounter++)
            {
                BDD * from = new BDD(*tmpresult[acounter]);
                BDD * to = new BDD(*tmpresult[acounter + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
                BDD actions = timesTrans(from, to);
                //cout << "actions: ";
                //actions.print(a->count(), 2);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                BDD action = actions.PickOneMinterm(*a);
                if (acounter == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index,
                                (tmpresult[acounter])));
                    desc.push_back(index);
                    //desc.push_back(++scount);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount,
                            (tmpresult[acounter])));
                    desc.push_back(scount++);
                    //desc.push_back(++scount);
                }
                //countex->push_back(new vector<int>(desc));

                //	position++;
            }

            // Now add the loop back

            BDD * from = new BDD(*tmpresult[numberofstates]);
            BDD * to = new BDD(*tmpresult[loopstart]);
            (*to) = to->SwapVariables(*v, *pv);
            //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
            BDD actions = timesTrans(from, to);
            actions = Exists(v, actions);
            actions = Exists(pv, actions);
            BDD action = actions.PickOneMinterm(*a);
            //desctr.push_back(new transition(from,position,to,loopstart,1,&action));

            if (loopstart == 0)
            {
                if (numberofstates == 0)
                {
                    desctr.push_back(new transition(from, index, to, index,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));

                    desc.push_back(index);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, index,
                            &action));
                    idbdd->insert(pair<int, BDD *> (scount,
                            (tmpresult[numberofstates])));

                    desc.push_back(scount);
                }
                desc.push_back(index);
            }
            else
            {
                int loopposition = position1 + loopstart;
                desctr.push_back(new transition(from, scount, to, loopposition,
                        &action));

                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[numberofstates])));
                desc.push_back(scount);
                desc.push_back(loopposition);
            }
            countex->push_back(new vector<int> (desc));

            cextr->push_back(new vector<transition *> (desctr));

            //scount += position;

            /*int totstates = 0;

             bool buildingprefix = true;

             for(vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri != tmpresult.end(); tmpri++) {
             desc.push_back(scount);
             idbdd->insert(pair<int, BDD *>(scount, (*tmpri) ) );
             if ( ( (*(*tmpri)) <= Q ) && ( buildingprefix ) ) {
             // found first state of the loop
             buildingprefix = false;
             // Add <id,id...> to countex
             countex->push_back(new vector<int>(desc));
             cout << " < ";
             for(int j=0; j<(int)desc.size(); j++)
             cout << desc.at(j);
             cout << " > " << endl;
             desc.clear();
             desc.push_back(scount);

             }
             scount++;
             totstates++;
             }

             scount--;

             // For the loop
             //desc.push_back(scount-1);
             desc.push_back(loopposition);
             countex->push_back(new vector<int>(desc));
             cout << " < ";
             for(int j=0; j<(int)desc.size(); j++)
             cout << desc.at(j);
             cout << " > " << endl;*/

            // Print witness for all states in the path

            for (vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri
                    != tmpresult.end(); tmpri++)
            {
                if ((*(*tmpri)) <= ((modal_formula *) obj[0])->check_formula())
                {
                    if (tmpri == tmpresult.begin())
                        ((modal_formula *) obj[0])->build_cex(*tmpri, index);
                    else
                        ((modal_formula *) obj[0])->build_cex(*tmpri,
                                ++position1);
                }
            }

            //scount--;

            return true;

        }
        case 13: // EX
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in EX" << endl;
            }
            /* TODO: check fairness here */
            tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation

            BDD p = ((modal_formula *) obj[0])->check_formula();

            p = p.SwapVariables(*pv, *v); // The set of "next" states where p is true.


            //BDD aset1 = (*state)*RT; // the set of states reachable from "state"
            BDD aset1 = timesRT(state);

            aset1 = aset1 * p; // the set above where, additionally, p holds

            aset1 = aset1.SwapVariables(*v, *pv); // swap back

            BDD curstate = aset1.PickOneMinterm(*v);
            tmpresult.push_back(new BDD(curstate));

            // Now populate the table with id -> BDD

            /*int totstates = 0;
             for(vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri != tmpresult.end(); tmpri++) {
             desc.push_back(scount);
             idbdd->insert(pair<int, BDD *>(scount, (*tmpri) ) );
             scount++;
             totstates++;
             }
             scount--;

             // Add <id,id...> to countex
             countex->push_back(new vector<int>(desc));

             // Now building the vector for transitions

             int position = scount - totstates + 1;

             for (int i=0; i < (int)tmpresult.size()-1; i++) {
             BDD * from = new BDD(*tmpresult[i]);
             BDD * to = new BDD(*tmpresult[i+1]);
             (*to) = to->SwapVariables(*v,*pv);
             //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
             BDD actions = timesTrans(from, to);
             actions = Exists(v,actions);
             actions = Exists(pv,actions);
             BDD action = actions.PickOneMinterm(*a);
             desctr.push_back(new transition(from,position,to,position+1,1,&action));
             position++;
             }
             */
            BDD * from = new BDD(*tmpresult[0]);
            BDD * to = new BDD(*tmpresult[1]);
            (*to) = to->SwapVariables(*v, *pv);
            BDD actions = timesTrans(from, to);
            actions = Exists(v, actions);
            actions = Exists(pv, actions);
            BDD action = actions.PickOneMinterm(*a);
            desctr.push_back(new transition(from, index, to, scount + 1,
                    &action));
            if (index >= idbdd->size())
                idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            desc.push_back(index);
            desc.push_back(++scount);
            countex->push_back(new vector<int> (desc));
            idbdd->insert(pair<int, BDD *> (scount, (tmpresult[1])));
            cextr->push_back(new vector<transition *> (desctr));

            return ((modal_formula *) obj[0])->build_cex(tmpresult[1], scount);
        }
        case 15: // EF
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in EF" << endl;
            }
            /* TODO: check fairness here */

            //tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation
            BDD p = ((modal_formula *) obj[0])->check_formula();
            BDD tmp = bddmgr->bddOne();
            BDD q = bddmgr->bddZero();
            BDD curstate = bddmgr->bddOne(); // the current state

            int n = 0;

            while (q != tmp)
            {
                tmp = q;
                q = p + check_EX(tmp);
                S.push_back(new BDD(q * reach));
                n++;
            }

            int j = 0;

            while (!(curstate <= (*(S[0]))))
            {
                BDD aset1;
                if (j == 0)
                {
                    aset1 = (*state);
                }
                else
                {
                    //aset1 = Exists(v, (curstate)*RT);
                    aset1 = Exists(v, timesRT(&curstate));
                    aset1 = aset1.SwapVariables(*v, *pv);
                }
                BDD aset2 = aset1 * (*(S[n - j - 1]));

                if (aset2 == bddmgr->bddZero())
                {
                    return false;
                }
                curstate = aset2.PickOneMinterm(*v);
                tmpresult.push_back(new BDD(curstate));

                j++;

            }

            // Now populate the table with id -> BDD
            /*int totstates = 0;
             for(vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri != tmpresult.end(); tmpri++) {
             desc.push_back(scount);
             idbdd->insert(pair<int, BDD *>(scount, (*tmpri) ) );
             scount++;
             totstates++;
             }

             scount--;

             // Add <id,id...> to countex
             countex->push_back(new vector<int>(desc));

             int position = scount - totstates + 1;
             //cout << "in EF: position = " << position << endl;

             if ( options["debug"] == 1 ) {
             cout << "DEBUG in build_cex in EF, position is " << position << " and tmpresult is " << tmpresult.size() << endl;
             }*/

            // building transitions
            for (int i = 0; i < (int) tmpresult.size() - 1; i++)
            {
                BDD * from = new BDD(*tmpresult[i]);
                BDD * to = new BDD(*tmpresult[i + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
                BDD actions = timesTrans(from, to);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                BDD action = actions.PickOneMinterm(*a);
                if (i == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[i])));
                    desc.push_back(index);
                    //desc.push_back(++scount);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount, (tmpresult[i])));
                    desc.push_back(scount++);
                    //desc.push_back(++scount);
                }
                //countex->push_back(new vector<int>(desc));
                //desctr.push_back(new transition(from,position,to,position+1,1,&action));
                //position++;
            }
            if (tmpresult.size() == 1)
            {
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            }
            else
            {
                desc.push_back(scount);
                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[tmpresult.size() - 1])));
                countex->push_back(new vector<int> (desc));
                cextr->push_back(new vector<transition *> (desctr));
            }

            return ((modal_formula *) obj[0])->build_cex(
                    tmpresult[tmpresult.size() - 1],
                    (tmpresult.size() == 1 ? index : scount));
        }
        case 17: // EU
        {

            /* check_EU(p,q) :
             BDD W = p;
             BDD X = reach;
             BDD Y = q;
             while ( X != Y ) {
             X = Y;
             Y = Y + (W * check_EX(Y));
             }
             return Y;
             */

            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex in EU" << endl;
            }
            /* TODO: check fairness here */

            //tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation

            BDD p = ((modal_formula *) obj[0])->check_formula();
            BDD q = ((modal_formula *) obj[1])->check_formula();

            BDD tmp1 = bddmgr->bddOne();
            BDD curstate = bddmgr->bddOne(); // the current state

            int n = 0;

            // W = p; X = tmp1; Y = tmp2

            BDD tmp2 = q;
            while (tmp1 != tmp2)
            {
                tmp1 = tmp2;
                tmp2 = tmp2 + (p * check_EX(tmp2));
                //S.push_back(new BDD(tmp2*reach));
                S.push_back(new BDD(tmp1));
                n++;
            }

            int j = 0;

            while (!(curstate <= (*(S[0]))))
            {
                BDD aset1;
                if (j == 0)
                {
                    aset1 = (*state);
                }
                else
                {
                    //aset1 = Exists(v, (curstate)*RT);
                    aset1 = Exists(v, timesRT(&curstate));
                    aset1 = aset1.SwapVariables(*v, *pv);
                }
                BDD aset2 = aset1 * (*(S[n - j - 1]));

                if (aset2 == bddmgr->bddZero())
                {
                    return false;
                }
                curstate = aset2.PickOneMinterm(*v);

                /* print state */
                /*for(unsigned int i=0; i<agents->size(); i++) {
                 cout << "Agent " << (*agents)[i]->get_name() << endl;
                 (*agents)[i]->print_state("  ", curstate, *v);
                 }*/
                /* print state */
                tmpresult.push_back(new BDD(curstate));

                j++;

            }

            /*int totstates = 0;
             // Now populate the table with id -> BDD
             for(vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri != tmpresult.end(); tmpri++) {
             desc.push_back(scount);
             idbdd->insert(pair<int, BDD *>(scount, (*tmpri) ) );
             scount++;
             totstates++;
             }

             scount--;

             // Add <id,id...> to countex
             countex->push_back(new vector<int>(desc));

             int position = scount - totstates + 1;*/

            int position1 = scount;

            // transitions
            for (int i = 0; i < (int) tmpresult.size() - 1; i++)
            {
                BDD * from = new BDD(*tmpresult[i]);
                BDD * to = new BDD(*tmpresult[i + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
                BDD actions = timesTrans(from, to);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                //cout << "in EU 1: action: ";
                //cout.flush();
                BDD action = actions.PickOneMinterm(*a);
                //action.print(a->count(), 2);
                if (i == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[i])));
                    desc.push_back(index);
                    //desc.push_back(++scount);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount, (tmpresult[i])));
                    desc.push_back(scount++);
                    //desc.push_back(++scount);
                }
                //desctr.push_back(new transition(from,position,to,position+1,1,&action));
                //position++;
            }
            if (tmpresult.size() == 1)
            {
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            }
            else
            {
                desc.push_back(scount);
                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[tmpresult.size() - 1])));
                countex->push_back(new vector<int> (desc));

                cextr->push_back(new vector<transition *> (desctr));
            }

            // The set of states reachable from the last state
            //BDD aset1 = Exists(v, (curstate)*RT);
            /*BDD aset1 = Exists(v, timesRT(&curstate));

             aset1 = aset1.SwapVariables(*v, *pv)*q;

             //cout << "in EU 2: somestate: ";
             //cout.flush();
             BDD somestate = aset1.PickOneMinterm(*v);
             //somestate.print(a->count(), 2);

             if ( ((modal_formula *)obj[1])->build_cex(&somestate, tmpresult.size() - 1) ) {
             return true;
             } else {
             return false;
             }*/// Do not understand the code above. tmpresult[tmpsult.size-1] should be a state that satisfies q.

            for (unsigned int i = 0; i < tmpresult.size() - 1; i++)
            {
                if ((*tmpresult[i])
                        <= ((modal_formula *) obj[0])->check_formula())
                {
                    if (i == 0)
                        ((modal_formula *) obj[0])->build_cex(tmpresult[i],
                                index);
                    else
                        ((modal_formula *) obj[0])->build_cex(tmpresult[i],
                                ++position1);
                }
            }
            return ((modal_formula *) obj[1])->build_cex(
                    tmpresult[tmpresult.size() - 1],
                    (tmpresult.size() == 1 ? index : scount));
        }

        case 0:
        case 10: // AG
        case 12: // AX
        case 14: // AF
        case 16: // AU
        case 30:
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex, checking atomic proposition"
                        << endl;
            }

            BDD p = check_formula();
            /*BDD rel;
             string name, name1;
             Object *id, *id1;
             if(op == 0)
             p = check_formula();
             else if(op == 30) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = !check_nK(!((modal_formula*)obj[1])->
             check_formula()*reach, er[name]) * reach;
             } else if(op == 31) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_GK(((modal_formula*)obj[1])->
             check_formula(), gm[name]);
             } else if(op == 32) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_GCK(((modal_formula*)obj[1])->
             check_formula(), gm[name]) * reach;
             } else if(op == 41) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             id1 = ((modal_formula*)obj[1])->get_operand(0);
             name1 = ((atomic_proposition *)id1)->get_proposition();
             if(is_agents->find(name1)!=is_agents->end())
             rel = deor[name1];
             else
             rel = deogm[name1];
             p = !check_nKH(!((modal_formula*)obj[2])->
             check_formula()*reach, er[name], rel)* reach;
             } else if(op == 42) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_DK(((modal_formula*)obj[1])->
             check_formula(), distgm[name]);
             } else if(op == 43) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             id1 = ((modal_formula*)obj[1])->get_operand(0);
             name1 = ((atomic_proposition *)id1)->get_proposition();
             if(is_agents->find(name1)!=is_agents->end())
             rel = deor[name1];
             else
             rel = deogm[name1];
             p = !check_nDKH(!((modal_formula*)obj[2])->
             check_formula()*reach, distgm[name], rel)* reach;
             }*/

            if ((*state) <= p)
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula is true in state" << endl;
                }

                if (idbdd->size() == 0)
                {
                    idbdd->insert(pair<int, BDD *> (index, state));
                    desc.push_back(index);
                    countex->push_back(new vector<int> (desc));
                }

                return true;
            }
            else
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula is false in state" << endl;
                }
                return false;
            }

        }

            // leaf
        case 3:
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex, checking negation" << endl;
            }

            /*
             * TODO: FRANCO, fix for epistemic operators
             */

            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex checking negation" << endl;
            }

            modal_formula * argument = ((modal_formula *) obj[0]);

            if (argument->get_op() == 0)
            {

                // It's the negation of an atom

                if (options["debug"] == 1)
                {
                    cout << "DEBUG in build_cex checking negation of an atom"
                            << endl;
                }

                BDD p = check_formula();

                if ((*state) <= p)
                {
                    if (options["debug"] == 1)
                    {
                        cout
                                << "DEBUG the negation of the formula is true in state"
                                << endl;
                    }

                    if (idbdd->size() == 0)
                    {
                        idbdd->insert(pair<int, BDD *> (index, state));
                        desc.push_back(index);
                        countex->push_back(new vector<int> (desc));
                    }

                    //return false;
                    return true;
                }
                else
                {
                    if (options["debug"] == 1)
                    {
                        cout
                                << "DEBUG the negation of the formula is false in state"
                                << endl;
                    }
                    //return true;
                    return false;
                }
            }
            else if (argument->get_op() == 30 || argument->get_op() == 31
                    || argument->get_op() == 40 || argument->get_op() == 32
                    || argument->get_op() == 41 || argument->get_op() == 42
                    || argument->get_op() == 43)
            {
                // it's the negation of K
                if (options["debug"] == 1)
                {
                    cout
                            << "DEBUG in build_cex checking negation of a K operator: "
                            << endl;
                }
                /* TODO: check fairness here */
                tmpresult.push_back(state);

                // Finding the position of the agent:
                //int whichagent = 0;
                string name, name1;
                Object *id, *id1;
                modal_formula *agentid =
                        (modal_formula *) (argument->get_operand(0));
                modal_formula *agentid1;
                BDD aset1;
                BDD rel;
                BDD formula;
                if (argument->get_op() == 30)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) (argument->get_operand(1)))-> check_formula()
                                    * reach;
                    /*aset1 = check_nK(formula, er[name]) * reach;

                     aset1 = aset1 * formula;
                     aset1 = get_K_states(aset1, state, name);*/

                    aset1 = get_K_states(formula, state, name);
                    /*if(rel!=aset1) {
                     cout << "The new algorithm for computing nK is wrong! -- " << to_string() << endl;
                     }
                     else {
                     cout << "The new algorithm for computing nK is correct! -- " << endl;
                     }*/
                }
                else if (argument->get_op() == 31)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) (argument->get_operand(1)))-> check_formula()
                                    * reach;
                    aset1 = check_nGK(formula, gm[name]) * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_GK_states(aset1, state, name);
                }
                else if (argument->get_op() == 32)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = ((modal_formula*) (argument->get_operand(1)))-> check_formula();
                    aset1 = !check_GCK(formula, gm[name]) * reach;

                    aset1 = aset1 * !formula;
                    aset1 = get_GK_states(aset1, state, name);
                }
                else if (argument->get_op() == 40)
                { // O
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) (argument->get_operand(1)))-> check_formula()
                                    * reach;
                    aset1 = check_nO(formula, deor[name]) * reach;
                }
                else if (argument->get_op() == 41)
                { // KH
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    agentid1 = (modal_formula *) (argument->get_operand(1));
                    id1 = agentid1->get_operand(0);
                    name1 = ((atomic_proposition *) id1)->get_proposition();
                    if (is_agents->find(name1) != is_agents->end())
                        rel = deor[name1];
                    else
                        rel = deogm[name1];
                    formula
                            = !((modal_formula*) argument->get_operand(2))-> check_formula()
                                    * reach;
                    aset1 = check_nKH(formula, er[name], rel) * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_K_states(aset1, state, name);
                    if (is_agents->find(name1) != is_agents->end())
                        aset1 = get_agent_greenstates(aset1, name1);
                    else
                        aset1 = get_group_greenstates(aset1, name1);
                }
                else if (argument->get_op() == 42)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) argument->get_operand(1))-> check_formula()
                                    * reach;
                    aset1 = check_nDK(formula, distgm[name]) * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_DK_states(aset1, state, name);
                }
                else if (argument->get_op() == 43)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    agentid1 = (modal_formula *) (argument->get_operand(1));
                    id1 = agentid1->get_operand(0);
                    name1 = ((atomic_proposition *) id1)->get_proposition();
                    if (is_agents->find(name1) != is_agents->end())
                        rel = deor[name1];
                    else
                        rel = deogm[name1];
                    formula
                            = !((modal_formula*) argument->get_operand(2))-> check_formula()
                                    * reach;
                    aset1 = check_nDKH(formula, distgm[name], rel) * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_DK_states(aset1, state, name);
                    if (is_agents->find(name1) != is_agents->end())
                        aset1 = get_agent_greenstates(aset1, name1);
                    else
                        aset1 = get_group_greenstates(aset1, name1);
                }

                if (aset1 == bddmgr->bddZero())
                    return false;

                BDD curstate = aset1.PickOneMinterm(*v);
                if (curstate == *state)
                {
                    aset1 = aset1 - curstate;
                    if (aset1 != bddmgr->bddZero())
                        curstate = aset1.PickOneMinterm(*v);
                }
                tmpresult.push_back(new BDD(curstate));

                // Now populate the table with id -> BDD

                /*int totstates = 0;
                 for(vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri != tmpresult.end(); tmpri++) {
                 desc.push_back(scount);
                 idbdd->insert(pair<int, BDD *>(scount, (*tmpri) ) );
                 scount++;
                 totstates++;
                 }
                 scount--;

                 // Add <id,id...> to countex
                 countex->push_back(new vector<int>(desc));

                 // Now building the vector for transitions

                 int position = scount - totstates + 1;*/

                /*for(unsigned int i=0; i<agents->size(); i++) {
                 if ( name == (*agents)[i]->get_name() ) {
                 whichagent = i;
                 }
                 }*/

                //for (int i=0; i < (int)tmpresult.size()-1; i++) {
                BDD * from = new BDD(*tmpresult[0]);
                BDD * to = new BDD(*tmpresult[1]);
                (*to) = to->SwapVariables(*v, *pv);
                //BDD * actions = new BDD(preRT*andprot*(*from)*(*to));
                /*BDD actions = timesTrans(from, to);
                 actions = Exists(v,actions);
                 actions = Exists(pv,actions);
                 BDD action = actions.PickOneMinterm(*a);*/
                BDD action = bddmgr->bddOne();
                if (argument->get_op() == 30 || argument->get_op() == 31
                        || argument->get_op() == 32 || argument->get_op() == 40
                        || argument->get_op() == 42)
                    desctr.push_back(new transition(from, index, to,
                            scount + 1, name, &action));
                else if (argument->get_op() == 41 || argument->get_op() == 43)
                    desctr.push_back(new transition(from, index, to,
                            scount + 1, name, name1, &action));
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
                desc.push_back(index);
                desc.push_back(++scount);
                countex->push_back(new vector<int> (desc));
                // a transition with a negative value is an epistemic relation,
                // index being the number of the agent in agents vector.
                //position++;
                //}
                idbdd->insert(pair<int, BDD *> (scount, (tmpresult[1])));

                cextr->push_back(new vector<transition *> (desctr));
                if (argument->get_op() != 40)
                {
                    modal_formula * fcex;
                    if (argument->get_op() == 30 || argument->get_op() == 31
                            || argument->get_op() == 32 || argument->get_op()
                            == 42)
                        fcex = new modal_formula(3,
                                ((modal_formula*) (argument->get_operand(1))));
                    else
                        fcex = new modal_formula(3,
                                ((modal_formula*) (argument->get_operand(2))));
                    fcex = fcex->push_negations(1);

                    //cout << fcex->to_string() << endl;

                    return fcex->build_cex(tmpresult[1], scount);
                }
                else
                    return true;
            }
        }
        default:
        {
            if (options["quiet"] == 0)
                cout
                        << " OPERATOR CURRENTLY NOT SUPPORTED IN WITNESS/COUNTEREXAMPLE";
            return false;
        }
    }
    if (options["quiet"] == 0)
        cout
                << " AN ERROR HAS OCCURREND IN THE GENERATION OF WITNESS/COUNTEREXAMPLE";
    return false;

}

bool modal_formula::build_cex_fair(BDD * state, unsigned int index,
        BDD fair_reach)
{

    /* TODO: Add fairness */

    vector<BDD *> tmpresult; // a vector to store the states of the witness
    vector<int> desc; // This is a vector of state id (see global variables countex and idbdd)
    vector<transition *> desctr; // This is a vector of transitions (see golbal var cextr)


    if (options["debug"] == 1)
    {
        cout << "DEBUG in build_cex with op = " << (int) op << endl;
    }

    switch (op)
    {
        case 1: // AND
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in AND: " << to_string()
                        << endl;
            }
            bool r2 = ((modal_formula*) obj[1])->build_cex_fair(state, index,
                    fair_reach);
            if (!r2)
                return false;
            bool r1 = ((modal_formula*) obj[0])->build_cex_fair(state, index,
                    fair_reach);
            if (!r1)
                return false;
            return true;
            break;
        }
        case 2: // OR
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in OR" << endl;
            }
            bool r1;
            modal_formula * left = ((modal_formula*) obj[1]);
            BDD * res = new BDD();
            (*res) = left->check_formula_fair(fair_reach);

            if ((*state) <= (*res))
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula " << left->to_string()
                            << " is true in state " << endl;
                }
                r1 = left->build_cex_fair(state, index, fair_reach);
                if (!r1)
                    return false;
            }
            else
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula " << left->to_string()
                            << " is false in state " << endl;
                }
                modal_formula * right = ((modal_formula*) obj[0]);
                r1 = right->build_cex_fair(state, index, fair_reach);
            }
            return r1;
            break;
        }
        case 11: // EG
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in EG" << endl;
            }
            // Need to find a cycle here

            BDD last = check_formula_fair(fair_reach); // the last state of fixpoint computation

            if (!(*state <= last))
                return false;

            /* TODO: check fairness here */
            tmpresult.push_back(new BDD(*state));

            vector<BDD *> S; // a vector to store the stages of the computation

            int j = 0;

            BDD Q = bddmgr->bddZero();
            BDD T = bddmgr->bddZero() + *state;

            while (Q == bddmgr->bddZero())
            {

                j++;

                BDD reachablefromlast = timesRT(tmpresult[j - 1]);

                reachablefromlast = Exists(v, reachablefromlast);
                reachablefromlast = reachablefromlast.SwapVariables(*v, *pv);

                BDD abdd = reachablefromlast * last;
                if (abdd == bddmgr->bddZero())
                {
                    return false;
                }

                Q = abdd * T; // if this is not false, we found a loop
                if (Q == bddmgr->bddZero())
                {
                    BDD curstate = abdd.PickOneMinterm(*v);

                    tmpresult.push_back(new BDD(curstate));

                    T = T + curstate;
                }
                else
                {
                    break;
                }
            }

            unsigned int numberofstates = (unsigned int) tmpresult.size() - 1; // (the last one is NOT repeated)

            int loopstart = -1; // the position where the loop starts

            for (unsigned int acounter = 0; acounter <= numberofstates; acounter++)
            {
                if ((Q * (*tmpresult[acounter])) != bddmgr->bddZero())
                {
                    loopstart = acounter;
                    break;
                }
            }

            if (loopstart == -1)
            {
                if (options["quiet"] == 0)
                {
                    cout << "Witness generation for EG:" << endl;
                    cout << "THERE IS A PROBLEM HERE, PLEASE REPORT THIS ERROR"
                            << endl;
                }
                return false;
            }

            // building transitions
            // first go to the last loop state
            int position1 = scount;
            for (unsigned int acounter = 0; acounter < numberofstates; acounter++)
            {
                BDD * from = new BDD(*tmpresult[acounter]);
                BDD * to = new BDD(*tmpresult[acounter + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                BDD actions = timesTrans(from, to);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                BDD action = actions.PickOneMinterm(*a);
                if (acounter == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index,
                                (tmpresult[acounter])));
                    desc.push_back(index);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount,
                            (tmpresult[acounter])));
                    desc.push_back(scount++);
                }
            }

            // Now add the loop back

            BDD * from = new BDD(*tmpresult[numberofstates]);
            BDD * to = new BDD(*tmpresult[loopstart]);
            (*to) = to->SwapVariables(*v, *pv);
            BDD actions = timesTrans(from, to);
            actions = Exists(v, actions);
            actions = Exists(pv, actions);
            BDD action = actions.PickOneMinterm(*a);

            if (loopstart == 0)
            {
                if (numberofstates == 0)
                {
                    desctr.push_back(new transition(from, index, to, index,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));

                    desc.push_back(index);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, index,
                            &action));
                    idbdd->insert(pair<int, BDD *> (scount,
                            (tmpresult[numberofstates])));

                    desc.push_back(scount);
                }
                desc.push_back(index);
            }
            else
            {
                int loopposition = position1 + loopstart;
                desctr.push_back(new transition(from, scount, to, loopposition,
                        &action));

                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[numberofstates])));
                desc.push_back(scount);
                desc.push_back(loopposition);
            }
            countex->push_back(new vector<int> (desc));

            cextr->push_back(new vector<transition *> (desctr));

            // Print witness for all states in the path

            for (vector<BDD *>::iterator tmpri = tmpresult.begin(); tmpri
                    != tmpresult.end(); tmpri++)
            {
                if ((*(*tmpri))
                        <= ((modal_formula *) obj[0])->check_formula_fair(
                                fair_reach))
                {
                    if (tmpri == tmpresult.begin())
                        ((modal_formula *) obj[0])->build_cex_fair(*tmpri,
                                index, fair_reach);
                    else
                        ((modal_formula *) obj[0])->build_cex_fair(*tmpri,
                                ++position1, fair_reach);
                }
            }
            return true;

        }
        case 13: // EX
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in EX" << endl;
            }
            /* TODO: check fairness here */
            tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation

            BDD p = ((modal_formula *) obj[0])->check_formula_fair(fair_reach);

            //if(!(*state <= p) )
            //	return false;

            p = p.SwapVariables(*pv, *v); // The set of "next" states where p is true.

            BDD aset1 = timesRT(state); // the set of states reachable from "state"

            aset1 = aset1 * p; // the set above where, additionally, p holds

            aset1 = aset1.SwapVariables(*v, *pv); // swap back

            BDD curstate = aset1.PickOneMinterm(*v);
            tmpresult.push_back(new BDD(curstate));

            // Now populate the table with id -> BDD

            BDD * from = new BDD(*tmpresult[0]);
            BDD * to = new BDD(*tmpresult[1]);
            (*to) = to->SwapVariables(*v, *pv);
            BDD actions = timesTrans(from, to);
            actions = Exists(v, actions);
            actions = Exists(pv, actions);
            BDD action = actions.PickOneMinterm(*a);
            desctr.push_back(new transition(from, index, to, scount + 1,
                    &action));
            if (index >= idbdd->size())
                idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            desc.push_back(index);
            desc.push_back(++scount);
            countex->push_back(new vector<int> (desc));
            idbdd->insert(pair<int, BDD *> (scount, (tmpresult[1])));
            cextr->push_back(new vector<transition *> (desctr));

            if (((modal_formula *) obj[0])->build_cex_fair(tmpresult[1],
                    scount, fair_reach))
            {
                return true;
            }
            else
            {
                return false;
            }

        }
        case 15: // EF
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in EF: " << to_string()
                        << endl;
            }
            /* TODO: check fairness here */

            //tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation

            BDD p = ((modal_formula *) obj[0])->check_formula_fair(fair_reach);
            BDD tmp = bddmgr->bddOne();
            BDD q = bddmgr->bddZero();
            BDD curstate = bddmgr->bddOne(); // the current state
            //if(!(*state <= p) )
            //	return false;

            int n = 0;

            while (q != tmp)
            {
                tmp = q;
                q = p + check_EX_fair(tmp, fair_reach);
                S.push_back(new BDD(q * fair_reach));
                n++;
            }

            int j = 0;

            while (!(curstate <= (*(S[0]))))
            {
                BDD aset1;
                if (j == 0)
                {
                    aset1 = (*state);
                }
                else
                {
                    aset1 = Exists(v, timesRT(&curstate));
                    aset1 = aset1.SwapVariables(*v, *pv);
                }
                BDD aset2 = aset1 * (*(S[n - j - 1]));

                if (aset2 == bddmgr->bddZero())
                {
                    return false;
                }
                curstate = aset2.PickOneMinterm(*v);
                tmpresult.push_back(new BDD(curstate));

                j++;

            }

            // building transitions
            for (int i = 0; i < (int) tmpresult.size() - 1; i++)
            {
                BDD * from = new BDD(*tmpresult[i]);
                BDD * to = new BDD(*tmpresult[i + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                BDD actions = timesTrans(from, to);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                BDD action = actions.PickOneMinterm(*a);
                if (i == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[i])));
                    desc.push_back(index);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount, (tmpresult[i])));
                    desc.push_back(scount++);
                }
            }
            if (tmpresult.size() == 1)
            {
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            }
            else
            {
                desc.push_back(scount);
                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[tmpresult.size() - 1])));
                countex->push_back(new vector<int> (desc));
                cextr->push_back(new vector<transition *> (desctr));
            }

            if (((modal_formula *) obj[0])->build_cex_fair(
                    tmpresult[tmpresult.size() - 1],
                    (tmpresult.size() == 1 ? index : scount), fair_reach))
            {
                return true;
            }
            else
            {
                return false;
            }

        }
        case 17: // EU
        {

            /* check_EU(p,q) :
             BDD W = p;
             BDD X = reach;
             BDD Y = q;
             while ( X != Y ) {
             X = Y;
             Y = Y + (W * check_EX(Y));
             }
             return Y;
             */

            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair in EU" << endl;
            }
            /* TODO: check fairness here */

            //tmpresult.push_back(state);

            vector<BDD *> S; // a vector to store the stages of the fixpoint computation

            BDD p = ((modal_formula *) obj[0])->check_formula_fair(fair_reach);
            BDD q = ((modal_formula *) obj[1])->check_formula_fair(fair_reach);

            if (!(*state <= p || *state <= q))
                return false;

            BDD tmp1 = bddmgr->bddOne();
            BDD curstate = bddmgr->bddOne(); // the current state

            int n = 0;

            // W = p; X = tmp1; Y = tmp2

            BDD tmp2 = q;
            while (tmp1 != tmp2)
            {
                tmp1 = tmp2;
                tmp2 = tmp2
                        + (p * check_EX_fair(tmp2, fair_reach) * fair_reach);
                //S.push_back(new BDD(tmp2*fair_reach));
                S.push_back(new BDD(tmp1));
                n++;
            }

            int j = 0;

            while (!(curstate <= (*(S[0]))))
            {
                BDD aset1;
                if (j == 0)
                {
                    aset1 = (*state);
                }
                else
                {
                    aset1 = Exists(v, timesRT(&curstate));
                    aset1 = aset1.SwapVariables(*v, *pv);
                }
                BDD aset2 = aset1 * (*(S[n - j - 1]));

                if (aset2 == bddmgr->bddZero())
                {
                    return false;
                }
                curstate = aset2.PickOneMinterm(*v);

                tmpresult.push_back(new BDD(curstate));

                j++;

            }

            int position1 = scount;

            // transitions
            for (int i = 0; i < (int) tmpresult.size() - 1; i++)
            {
                BDD * from = new BDD(*tmpresult[i]);
                BDD * to = new BDD(*tmpresult[i + 1]);
                (*to) = to->SwapVariables(*v, *pv);
                BDD actions = timesTrans(from, to);
                actions = Exists(v, actions);
                actions = Exists(pv, actions);
                BDD action = actions.PickOneMinterm(*a);
                if (i == 0)
                {
                    desctr.push_back(new transition(from, index, to, ++scount,
                            &action));
                    if (index >= idbdd->size())
                        idbdd->insert(pair<int, BDD *> (index, (tmpresult[i])));
                    desc.push_back(index);
                }
                else
                {
                    desctr.push_back(new transition(from, scount, to, scount
                            + 1, &action));
                    idbdd->insert(pair<int, BDD *> (scount, (tmpresult[i])));
                    desc.push_back(scount++);
                }
            }
            if (tmpresult.size() == 1)
            {
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
            }
            else
            {
                desc.push_back(scount);
                idbdd->insert(pair<int, BDD *> (scount,
                        (tmpresult[tmpresult.size() - 1])));
                countex->push_back(new vector<int> (desc));

                cextr->push_back(new vector<transition *> (desctr));
            }

            for (unsigned int i = 0; i < tmpresult.size() - 1; i++)
            {
                if ((*tmpresult[i])
                        <= ((modal_formula *) obj[0])->check_formula_fair(
                                fair_reach))
                {
                    if (i == 0)
                        ((modal_formula *) obj[0])->build_cex_fair(
                                tmpresult[i], index, fair_reach);
                    else
                        ((modal_formula *) obj[0])->build_cex_fair(
                                tmpresult[i], ++position1, fair_reach);
                }
            }
            if (((modal_formula *) obj[1])->build_cex_fair(
                    tmpresult[tmpresult.size() - 1],
                    (tmpresult.size() == 1 ? index : scount), fair_reach))
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        case 0:
        case 10: // AG
        case 12: // AX
        case 14: // AF
        case 16: // AU
        case 30:
        case 31:
        case 32:
        case 40:
        case 41:
        case 42:
        case 43:
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex_fair, checking atomic proposition"
                        << endl;
            }

            BDD p = check_formula_fair(fair_reach);
            /*BDD rel;
             string name, name1;
             Object *id, *id1;
             if(op == 0)
             p = check_formula_fair(fair_reach);
             else if(op == 30) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = !check_nK_fair(!((modal_formula*)obj[1])->
             check_formula_fair(fair_reach)*reach, er[name], fair_reach) * reach;
             } else if(op == 31) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_GK_fair(((modal_formula*)obj[1])->
             check_formula_fair(fair_reach), gm[name], fair_reach);
             } else if(op == 32) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_GCK_fair(((modal_formula*)obj[1])->
             check_formula_fair(fair_reach), gm[name], fair_reach) * reach;
             } else if(op == 41) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             id1 = ((modal_formula*)obj[1])->get_operand(0);
             name1 = ((atomic_proposition *)id1)->get_proposition();
             if(is_agents->find(name1)!=is_agents->end())
             rel = deor[name1];
             else
             rel = deogm[name1];
             p = !check_nKH_fair(!((modal_formula*)obj[2])->
             check_formula_fair(fair_reach)*reach, er[name], rel, fair_reach)* reach;
             } else if(op == 42) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             p = check_DK_fair(((modal_formula*)obj[1])->
             check_formula_fair(fair_reach), distgm[name], fair_reach);
             } else if(op == 43) {
             id = ((modal_formula*)obj[0])->get_operand(0);
             name = ((atomic_proposition *)id)->get_proposition();
             id1 = ((modal_formula*)obj[1])->get_operand(0);
             name1 = ((atomic_proposition *)id1)->get_proposition();
             if(is_agents->find(name1)!=is_agents->end())
             rel = deor[name1];
             else
             rel = deogm[name1];
             p = !check_nDKH_fair(!((modal_formula*)obj[2])->
             check_formula_fair(fair_reach)*reach, distgm[name], rel, fair_reach)* reach;
             }*/

            if ((*state) <= p)
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula is true in state" << endl;
                }

                if (idbdd->size() == 0)
                {
                    idbdd->insert(pair<int, BDD *> (index, state));
                    desc.push_back(index);
                    countex->push_back(new vector<int> (desc));
                }

                return true;
            }
            else
            {
                if (options["debug"] == 1)
                {
                    cout << "DEBUG the formula is false in state" << endl;
                }
                return false;
            }

        }

            // leaf
        case 3:
        {
            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex, checking negation" << endl;
            }

            /*
             * TODO: FRANCO, fix for epistemic operators
             */

            if (options["debug"] == 1)
            {
                cout << "DEBUG in build_cex checking negation" << endl;
            }

            modal_formula * argument = ((modal_formula *) obj[0]);

            if (argument->get_op() == 0)
            {

                // It's the negation of an atom

                if (options["debug"] == 1)
                {
                    cout << "DEBUG in build_cex checking negation of an atom"
                            << endl;
                }

                BDD p = check_formula_fair(fair_reach);

                if ((*state) <= p)
                {
                    if (options["debug"] == 1)
                    {
                        cout
                                << "DEBUG the negation of the formula is true in state"
                                << endl;
                    }

                    if (idbdd->size() == 0)
                    {
                        idbdd->insert(pair<int, BDD *> (index, state));
                        desc.push_back(index);
                        countex->push_back(new vector<int> (desc));
                    }

                    //return false;
                    return true;
                }
                else
                {
                    if (options["debug"] == 1)
                    {
                        cout
                                << "DEBUG the negation of the formula is false in state"
                                << endl;
                    }
                    return false;
                }
            }
            else if (argument->get_op() == 30 || argument->get_op() == 31
                    || argument->get_op() == 32 || argument->get_op() == 40
                    || argument->get_op() == 41 || argument->get_op() == 42
                    || argument->get_op() == 43)
            {
                // it's the negation of K
                if (options["debug"] == 1)
                {
                    cout
                            << "DEBUG in build_cex checking negation of a K operator: "
                            << endl;
                }
                /* TODO: check fairness here */
                tmpresult.push_back(state);

                // Finding the position of the agent:
                string name, name1;
                Object *id, *id1;
                modal_formula *agentid =
                        (modal_formula *) (argument->get_operand(0));
                modal_formula *agentid1;
                BDD aset1;
                BDD rel;
                BDD formula;

                if (argument->get_op() == 30)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    /*formula = !((modal_formula*)(argument->get_operand(1)))->
                     check_formula_fair(fair_reach)*reach;
                     aset1 = check_nK_fair(formula, er[name], fair_reach) * reach;
                     aset1 = aset1 * formula;
                     aset1 = get_K_states(aset1, state, name);*/

                    aset1
                            = get_K_states(
                                    !((modal_formula*) (argument->get_operand(1)))-> check_formula_fair(
                                            fair_reach) * fair_reach, state,
                                    name);
                    /*if(rel!=aset1) {
                     cout << "The new algorithm for computing nK is wrong! -- " << to_string() << endl;
                     }
                     else {
                     cout << "The new algorithm for computing nK is correct! -- " << endl;
                     }*/
                }
                else if (argument->get_op() == 31)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) (argument->get_operand(1)))-> check_formula_fair(
                                    fair_reach) * reach;
                    aset1 = check_nGK_fair(formula, gm[name], fair_reach)
                            * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_GK_states(aset1, state, name);
                }
                else if (argument->get_op() == 32)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = ((modal_formula*) (argument->get_operand(1)))-> check_formula_fair(
                                    fair_reach);
                    aset1 = !check_GCK_fair(formula, gm[name], fair_reach)
                            * reach;

                    aset1 = aset1 * !formula;
                    aset1 = get_GK_states(aset1, state, name);
                }
                else if (argument->get_op() == 40)
                { // O
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula
                            = !((modal_formula*) (argument->get_operand(1)))-> check_formula_fair(
                                    fair_reach) * reach;
                    aset1 = check_nO_fair(formula, deor[name], fair_reach)
                            * reach;
                }
                else if (argument->get_op() == 41)
                { // KH
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    agentid1 = (modal_formula *) (argument->get_operand(1));
                    id1 = agentid1->get_operand(0);
                    name1 = ((atomic_proposition *) id1)->get_proposition();
                    if (is_agents->find(name1) != is_agents->end())
                        rel = deor[name1];
                    else
                        rel = deogm[name1];
                    formula = !((modal_formula*) obj[2])-> check_formula_fair(
                            fair_reach) * reach;
                    aset1 = check_nKH_fair(formula, er[name], rel, fair_reach)
                            * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_K_states(aset1, state, name);
                }
                else if (argument->get_op() == 42)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    formula = !((modal_formula*) obj[1])-> check_formula_fair(
                            fair_reach) * reach;
                    aset1 = check_nDK_fair(formula, distgm[name], fair_reach)
                            * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_DK_states(aset1, state, name);
                }
                else if (argument->get_op() == 43)
                {
                    id = agentid->get_operand(0);
                    name = ((atomic_proposition *) id)->get_proposition();
                    agentid1 = (modal_formula *) (argument->get_operand(1));
                    id1 = agentid1->get_operand(0);
                    name1 = ((atomic_proposition *) id1)->get_proposition();
                    if (is_agents->find(name1) != is_agents->end())
                        rel = deor[name1];
                    else
                        rel = deogm[name1];
                    formula = !((modal_formula*) obj[2])-> check_formula_fair(
                            fair_reach) * reach;
                    aset1 = check_nDKH_fair(formula, distgm[name], rel,
                            fair_reach) * reach;

                    aset1 = aset1 * formula;
                    aset1 = get_DK_states(aset1, state, name);
                }

                if (aset1 == bddmgr->bddZero())
                    return false;

                BDD curstate = aset1.PickOneMinterm(*v);
                tmpresult.push_back(new BDD(curstate));

                BDD * from = new BDD(*tmpresult[0]);
                BDD * to = new BDD(*tmpresult[1]);
                (*to) = to->SwapVariables(*v, *pv);
                BDD action = bddmgr->bddOne();
                if (argument->get_op() == 30 || argument->get_op() == 31
                        || argument->get_op() == 32 || argument->get_op() == 42)
                    desctr.push_back(new transition(from, index, to,
                            scount + 1, name, &action));
                else if (argument->get_op() == 41 || argument->get_op() == 43)
                    desctr.push_back(new transition(from, index, to,
                            scount + 1, name, name1, &action));
                if (index >= idbdd->size())
                    idbdd->insert(pair<int, BDD *> (index, (tmpresult[0])));
                desc.push_back(index);
                desc.push_back(++scount);
                countex->push_back(new vector<int> (desc));
                idbdd->insert(pair<int, BDD *> (scount, (tmpresult[1])));

                cextr->push_back(new vector<transition *> (desctr));
                if (argument->get_op() != 40)
                {
                    modal_formula * fcex;
                    if (argument->get_op() == 30 || argument->get_op() == 31
                            || argument->get_op() == 40 || argument->get_op()
                            == 32 || argument->get_op() == 42)
                        fcex = new modal_formula(3,
                                ((modal_formula*) (argument->get_operand(1))));
                    else
                        fcex = new modal_formula(3,
                                ((modal_formula*) (argument->get_operand(2))));
                    fcex = fcex->push_negations(1);

                    return fcex->build_cex(tmpresult[1], scount);
                }
                else
                    return true;
            }
        }
        default:
        {
            if (options["quiet"] == 0)
                cout
                        << " OPERATOR CURRENTLY NOT SUPPORTED IN WITNESS/COUNTEREXAMPLE";
            return false;
        }
    }
    if (options["quiet"] == 0)
        cout
                << " AN ERROR HAS OCCURREND IN THE GENERATION OF WITNESS/COUNTEREXAMPLE";
    return false;

}

modal_formula* modal_formula::permute_agents(map<string, string> *permutation)
{
    switch (op)
    {
        case 0: // leaf
        {
            string name = ((atomic_proposition *) obj[0])->get_proposition();
            //string newname = permutation_name(name, permutation);
            //if(is_evaluation->find(newname) == is_evaluation->end()) {
            bool_expression* simple = is_evaluation->find(name)->second;
            bool_expression* tmpexpr = simple->permute_agents(permutation);
            string formula_str = tmpexpr->to_string();
            map<string, string>::iterator i = symmetry_atom_cache->find(
                    formula_str);
            if (i != symmetry_atom_cache->end())
                return new modal_formula(new atomic_proposition(new string(
                        i->second)));
            else
            {
                string newname = permutation_name(name, permutation);
                (*is_evaluation)[newname] = tmpexpr;
                (*symmetry_atom_cache)[formula_str] = newname;
                cout << newname << ": " << formula_str << endl;
                return new modal_formula(new atomic_proposition(new string(
                        newname)));
            }

            /*for(map<string, bool_expression*>::iterator i=is_evaluation->begin();
             i!=is_evaluation->end(); i++) {
             bool_expression* expr = i->second;
             if(expr->equal_to(tmpexpr))
             return new modal_formula(new atomic_proposition(new string(i->first)));
             }*/
            //(*is_evaluation)[newname] = tmpexpr;
            //}
            //return new modal_formula(new atomic_proposition(new string(newname)));
        }
        case 1: // AND
            return new modal_formula(1,
                    ((modal_formula*) obj[0])->permute_agents(permutation),
                    ((modal_formula*) obj[1])->permute_agents(permutation));
        case 2: // OR
            return new modal_formula(2,
                    ((modal_formula*) obj[0])->permute_agents(permutation),
                    ((modal_formula*) obj[1])->permute_agents(permutation));
        case 3: // NOT
            return new modal_formula(3,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 4: // IMPLIES
            return new modal_formula(4,
                    ((modal_formula*) obj[0])->permute_agents(permutation),
                    ((modal_formula*) obj[1])->permute_agents(permutation));
        case 10: // AG p = !EF !p
            return new modal_formula(10,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 11: // EG
            return new modal_formula(11,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 12: // AX p = ! EX !p
            return new modal_formula(12,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 13: // EX
            return new modal_formula(13,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 14: // AF p = !EG !p
            return new modal_formula(14,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 15: // EF p = p \lor EX EF p
            return new modal_formula(15,
                    ((modal_formula*) obj[0])->permute_agents(permutation));
        case 16: // AU (see check_AU)
            return new modal_formula(16,
                    ((modal_formula*) obj[0])->permute_agents(permutation),
                    ((modal_formula*) obj[1])->permute_agents(permutation));
        case 17: // EU
            return new modal_formula(17,
                    ((modal_formula*) obj[0])->permute_agents(permutation),
                    ((modal_formula*) obj[1])->permute_agents(permutation));
        case 30: // K
        {
            Object* id = ((modal_formula*) obj[0])->get_operand(0);
            string oldagent = ((atomic_proposition *) id)->get_proposition();
            string newagent = (*permutation)[oldagent];
            return new modal_formula(30, new modal_formula(
                    new atomic_proposition(new string(newagent))),
                    ((modal_formula*) obj[1])->permute_agents(permutation));

        }
        case 31: // Everybody knows
        case 32: // Common knowledge
        case 40: // O
        case 41: // KH
        case 42: // Distributed knowledge
        case 43: // Distributed knowledge assuming
        case 45: // ATL operator X
        case 46: // ATL operator F
        case 47: // ATL operator G
        case 48: // ATL operator U
            return this;
    }
    return this;
}

protocol_line::protocol_line(bool_expression *c, set<string> *a)
{
    condition = c;
    actions = a;
}
protocol_line::~protocol_line()
{
    cout << "deleting protocol_line " << to_string() << endl;
    //delete condition;
    //delete actions;
}
bool_expression* protocol_line::get_condition()
{
    return condition;
}
set<string>* protocol_line::get_actions()
{
    return actions;
}
string protocol_line::to_string()
{
    string str = "{ ";
    unsigned int k = 0;
    unsigned int j = (unsigned int) actions->size() - 1;
    for (set<string>::iterator i = actions->begin(); i != actions->end(); i++)
    {
        if (k == j)
            str += *i + " ";
        else
            str += *i + ", ";
        k++;
    }
    str += "}";
    return condition->to_string() + ": " + str;
}

assignment::assignment(string *name, expression *value)
{
    //agent_name = NULL;
    //var_name = name;
    var = new variable(name);
    var_value = value;
}
assignment::~assignment()
{
    cout << "deleting assignment " << to_string() << endl;
    //delete var;
    //delete var_value;
}
variable* assignment::get_var()
{
    return var;
}
expression* assignment::get_var_value()
{
    return var_value;
}
string assignment::to_string()
{
    return var->to_string() + " = " + var_value->to_string();
}
bool assignment::check_var_and_value(map<string, basictype *> *obsvars, map<
        string, basictype *> *vars)
{
    unsigned char right = var_value->get_type(); // right hand side
    unsigned char right1 = right;
    string vs = var->get_variable_name();
    map<string, basictype *>::iterator p = vars->find(vs);
    if (p == vars->end())
    {// the variable is not defined
        cout << "        variable " << vs << " is not defined." << endl;
        return false;
    }

    // add a link in variable to its type
    var->set_var_type(p->second);
    map<string, basictype *>::iterator p1;
    string vs1;
    if (right == 0)
    {
        vs1 = ((variable *) var_value)->get_variable_name();
        if (((variable *) var_value)->is_agent_name_null())
        {
            p1 = vars->find(vs1);
            if (p1 != vars->end())
            {// the variable is a local variable
                right = p1->second->get_type();
                ((variable *) var_value)->set_var_type(p1->second);
            }
        }
        else
        {
            string ag_name = ((variable *) var_value)->get_agent_name();
            if (ag_name == "Environment")
            {
                p1 = obsvars->find(vs1);
                if (p1 != obsvars->end())
                {// the variable is a global variable
                    right = p1->second->get_type();
                    ((variable *) var_value)->set_var_type(p1->second);
                }
            }
        }
    }
    unsigned char t1 = p->second->get_type(); //variable's type
    if ((t1 != right && right < 5 && !(t1 == 3 && right == 0)) || ((t1 == 1
            || t1 == 3) && right >= 5))
    {
        cout << "        variable " << vs << " has a wrong typed value."
                << endl;
        return false;
    }
    if (t1 == 1) // bool
        return true;
    else if (t1 == 2)
    {
        if (right1 == 0)
        { // rangedint
            int ub = ((rangedint *) (p->second))->get_upperbound();
            int lb = ((rangedint *) (p->second))->get_lowerbound();
            int ub1 = ((rangedint *) (p1->second))->get_upperbound();
            int lb1 = ((rangedint *) (p1->second))->get_lowerbound();
            if (ub < lb1 || ub1 < lb)
            {
                cout << "        variable " << vs1
                        << " cannot be assignment to variable " << vs << "."
                        << endl;
                return false;
            }
            else
                return true;
        }
        else if (right1 == 2)
        {// int_value
            if (((rangedint *) (p->second))->is_valid_value(
                    ((int_value *) var_value)->get_value()))
                return true;
            else
            {
                cout << "        variable " << vs
                        << " has a wrong integer value." << endl;
                return false;
            }
        }
        else
        {//arithmetic expression
            if (((arithmetic_expression *) var_value)->check_var_and_value(
                    obsvars, vars))
                return true;
        }
    }
    else if (t1 == 3)
    {// enum
        if (right == 0)
        { // an enum value
            if (((enumerate *) (p->second))->is_valid_value(vs1))
            {
                enum_value *tmp = new enum_value(new string(vs1));
                var_value = tmp; // change it to enum_value
                return true;
            }
            else
            {
                cout << "        variable " << vs
                        << " has a wrong enum value '" << vs1 << "'." << endl;
                return false;
            }
        }
        else
        { // an enumerate variable
            set<string> * s1 = ((enumerate *) (p->second))->get_enumvalue();
            set<string> * s2 = ((enumerate *) (p1->second))->get_enumvalue();
            if (s1->size() == s2->size())
            {// same size
                bool equal = true;
                for (set<string>::iterator i = s1->begin(); i != s1->end(); i++)
                    if (s2->find(*i) == s2->end())
                    {
                        equal = false;
                        break;
                    }
                if (equal)
                {
                    return true;
                }
                else
                {
                    cout << "        " << vs << " and " << vs1
                            << " do not have the same enumerate type." << endl;
                    return false;
                }
            }
            else
            {
                cout << "        " << vs << " and " << vs1
                        << " do not have the same enumerate type." << endl;
                return false;
            }
        }
    }
    return false;
}
BDD assignment::encode_bdd(BDD base)
{
    basictype *var_type = var->get_var_type();
    unsigned char value_type = var_type->get_type();
    int begin = var_type->get_index_begin();
    int end = var_type->get_index_end();
    BDD tmpbdd = base;
    unsigned char var_value_type = var_value->get_type();

    if (value_type == 1)
    { // boolean type
        if (var_value_type == 1)
        {
            if (((bool_value *) var_value)->get_value())
                tmpbdd = tmpbdd * (*pv)[begin];
            else
                tmpbdd = tmpbdd * !(*pv)[begin];
        }
        else
        {
            basictype *var_type1 = ((variable *) var_value)->get_var_type();
            int begin1 = var_type1->get_index_begin();
            // be careful here. rhs is in v and lhs is in pv
            tmpbdd *= ((!(*pv)[begin] + (*v)[begin1]) * ((*pv)[begin]
                    + !(*v)[begin1]));
        }
    }
    else if (value_type == 2)
    { // rangedint
        int upperbound = ((rangedint *) var_type)->get_upperbound();
        int lowerbound = ((rangedint *) var_type)->get_lowerbound();

        if (var_value_type == 0)
        { // a variable
            basictype *var_type1 = ((variable *) var_value)->get_var_type();
            int upperbound1 = ((rangedint *) var_type1)->get_upperbound();
            int lowerbound1 = ((rangedint *) var_type1)->get_lowerbound();
            if (upperbound1 > upperbound)
            {
                if (options["quiet"] == 0)
                    cout << "Warning: \"" << var_value->to_string()
                            << "\" might be greater than the upperbound of \""
                            << var->get_variable_name() << "\" in assignment "
                            << to_string() << endl;
            }
            if (lowerbound1 < lowerbound)
            {
                if (options["quiet"] == 0)
                    cout << "Warning: \"" << var_value->to_string()
                            << "\"  might be less than the lowerbound of \""
                            << var->get_variable_name() << "\" in assignment "
                            << to_string() << endl;
            }
            ADD rhs = ((rangedint *) var_type1)->build_ADD_tree();
            ADD lhs = ((rangedint *) var_type)->build_ADD_tree();
            lhs = lhs.SwapVariables(*addv, *addpv);
            ADD result = addEQ(lhs, rhs);
            tmpbdd *= result.BddThreshold(1);
        }
        else if (var_value_type == 2)
        { // an integer
            int value = ((int_value *) var_value)->get_value();
            vector<int>* vb = ((rangedint *) var_type)->get_value_index(value);
            for (int i = end; i >= begin; i--)
                if ((*vb)[i - begin] == 1)
                    tmpbdd = tmpbdd * (*pv)[i];
                else if ((*vb)[i - begin] == -1)
                    tmpbdd = tmpbdd * !(*pv)[i];
        }
        else if (var_value_type >= 5 && var_value_type <= 8)
        { // arithmetic expression
            ADD rhs = ((arithmetic_expression *) var_value)->build_ADD_tree();
            ADD overflow = addGT(rhs, bddmgr->constant(upperbound));
            if (overflow != bddmgr->addZero())
            {
                if (options["quiet"] == 0)
                    cout << "Warning: \"" << var_value->to_string()
                            << "\" might be greater than the upperbound of \""
                            << var->get_variable_name() << "\" in assignment "
                            << to_string() << endl;
            }
            ADD underflow = addLT(rhs, bddmgr->constant(lowerbound));
            if (underflow != bddmgr->addZero())
            {
                if (options["quiet"] == 0)
                    cout << "Warning: \"" << var_value->to_string()
                            << "\" might be less than the lowerbound of \""
                            << var->get_variable_name() << "\" in assignment "
                            << to_string() << endl;
            }
            ADD lhs = ((rangedint *) var_type)->build_ADD_tree();
            lhs = lhs.SwapVariables(*addv, *addpv);
            ADD result = addEQ(lhs, rhs);
            tmpbdd *= result.BddThreshold(1);
        }
    }
    else
    { // enumerate
        if (var_value_type == 3)
        {
            string value = ((enum_value *) var_value)->get_value();
            vector<bool>* vb = ((enumerate *) var_type)->get_value_index(value);
            for (int i = end; i >= begin; i--)
                if ((*vb)[i - begin])
                    tmpbdd = tmpbdd * (*pv)[i];
                else
                    tmpbdd = tmpbdd * !(*pv)[i];
        }
        else
        {
            basictype *var_type1 = ((variable *) var_value)->get_var_type();
            ADD rhs = ((enumerate *) var_type1)->build_ADD_tree();
            ADD lhs = ((enumerate *) var_type)->build_ADD_tree();
            lhs = lhs.SwapVariables(*addv, *addpv);
            ADD result = addEQ(lhs, rhs);
            tmpbdd *= result.BddThreshold(1);
        }
    }
    return tmpbdd;
}

evolution_line::evolution_line(vector<assignment *> *a, bool_expression *c)
{
    assignments = a;
    condition = c;
}
evolution_line::~evolution_line()
{
    cout << "deleting evolution_line " << to_string() << endl;
    //delete assignments;
    //delete condition;
}
vector<assignment *>* evolution_line::get_assignments()
{
    return assignments;
}
bool_expression* evolution_line::get_condition()
{
    return condition;
}
string evolution_line::to_string()
{
    string str = "";
    for (vector<assignment *>::iterator i = assignments->begin(); i
            != assignments->end(); i++)
        str += (*i)->to_string()
                + (i == assignments->end() - 1 ? " " : " and ");
    str += " if " + condition->to_string();
    return str;
}
BDD evolution_line::encode_bdd_assignements()
{
    BDD tmpbdd = bddmgr->bddOne();
    for (vector<assignment *>::iterator i = assignments->begin(); i
            != assignments->end(); i++)
        tmpbdd = (*i)->encode_bdd(tmpbdd);
    return tmpbdd;
}

bool evolution_line::check_double_assignment()
{
    bool flag = false;
    set<string> reassigned;
    for (unsigned int j = 0; j < assignments->size() - 1; j++)
    {
        string var_name = (*assignments)[j]->get_var()->get_variable_name();
        for (unsigned int k = j + 1; k < assignments->size(); k++)
        {
            string var_name1 =
                    (*assignments)[k]->get_var()->get_variable_name();
            if (var_name == var_name1)
            {
                reassigned.insert(var_name);
                flag = true;
                break;
            }
        }
    }
    if (reassigned.size() > 0)
    {
        for (set<string>::iterator i = reassigned.begin(); i
                != reassigned.end(); i++)
            cout << "      error: variable " << *i
                    << " is assigned twice or more" << endl;
    }
    return flag;
}

BDD evolution_line::encode_bdd_condition()
{
    BDD tmpbdd = (options["flatexpression"] == 1 || options["flatexpression"]
            == 3) ? condition->encode_bdd_flat(bddOne) : condition->encode_bdd(
            bddOne);
    return tmpbdd;
}

vector<evolution_line *> * evolution_line::extend_to_all_variables(map<string,
        basictype *> *allvars)
{
    vector<assignment *> *new_assignments;
    bool_expression *new_condition;
    vector<evolution_line *> *els = new vector<evolution_line *> ;
    els->push_back(this);
    // extend evolution to include all variables in assignments
    for (map<string, basictype *>::iterator j = allvars->begin(); j
            != allvars->end(); j++)
    {
        bool found = false;
        for (unsigned int k = 0; k < assignments->size(); k++)
        {
            variable* var = (*assignments)[k]->get_var();
            string varname = var->get_variable_name();
            if (varname == j->first)
            {
                found = true;
                break;
            }
        }

        if (!found)
        { // we add this variable to both sides
            unsigned int value_type = j->second->get_type();
            string *str = new string(j->first);
            variable* newvar = new variable(str);
            newvar->set_var_type(j->second);
            if (value_type == 1)
            { // boolean type
                vector<evolution_line *> *newels = new vector<evolution_line *> ;
                for (unsigned int k = 0; k < els->size(); k++)
                {
                    assignment *tmpass = new assignment(str, new bool_value(
                            false));
                    variable* vr = tmpass->get_var();
                    vr->set_var_type(j->second);
                    new_assignments = new vector<assignment *> (
                            (*els)[k]->get_assignments()->begin(),
                            (*els)[k]->get_assignments()->end());
                    new_assignments->push_back(tmpass);
                    logic_expression *tmplexp = new logic_expression(0, newvar,
                            new bool_value(false));
                    bool_expression *tmpbexp = new bool_expression(0, tmplexp);
                    new_condition = new bool_expression(1,
                            (*els)[k]->get_condition(), tmpbexp);
                    evolution_line* newline = new evolution_line(
                            new_assignments, new_condition);
                    newels->push_back(newline);
                    tmpass = new assignment(str, new bool_value(true));
                    vr = tmpass->get_var();
                    vr->set_var_type(j->second);
                    new_assignments = new vector<assignment *> (
                            (*els)[k]->get_assignments()->begin(),
                            (*els)[k]->get_assignments()->end());
                    new_assignments->push_back(tmpass);
                    tmplexp = new logic_expression(0, newvar, new bool_value(
                            true));
                    tmpbexp = new bool_expression(0, tmplexp);
                    new_condition = new bool_expression(1,
                            (*els)[k]->get_condition(), tmpbexp);
                    newline
                            = new evolution_line(new_assignments, new_condition);
                    newels->push_back(newline);
                }
                els = newels;
            }
            else if (value_type == 2)
            { // rangedint
                vector<evolution_line *> *newels = new vector<evolution_line *> ;
                rangedint *rint = (rangedint *) (j->second);
                for (unsigned int k = 0; k < els->size(); k++)
                    for (int t = rint->get_lowerbound(); t
                            <= rint->get_upperbound(); t++)
                    {
                        assignment *tmpass = new assignment(str, new int_value(
                                t));
                        variable* vr = tmpass->get_var();
                        vr->set_var_type(j->second);
                        new_assignments = new vector<assignment *> (
                                (*els)[k]->get_assignments()->begin(),
                                (*els)[k]->get_assignments()->end());
                        new_assignments->push_back(tmpass);
                        logic_expression *tmplexp = new logic_expression(0,
                                newvar, new int_value(t));
                        bool_expression *tmpbexp = new bool_expression(0,
                                tmplexp);
                        new_condition = new bool_expression(1,
                                (*els)[k]->get_condition(), tmpbexp);
                        evolution_line* newline = new evolution_line(
                                new_assignments, new_condition);
                        newels->push_back(newline);
                    }
                els = newels;
            }
            else
            { // enumerate
                vector<evolution_line *> *newels = new vector<evolution_line *> ;
                enumerate *enu = (enumerate *) (j->second);
                set<string> *val = enu->get_enumvalue();
                for (unsigned int k = 0; k < els->size(); k++)
                    for (set<string>::iterator t = val->begin(); t
                            != val->end(); t++)
                    {
                        string *s = new string(*t);
                        assignment *tmpass = new assignment(str,
                                new enum_value(s));
                        variable* vr = tmpass->get_var();
                        vr->set_var_type(j->second);
                        new_assignments = new vector<assignment *> (
                                (*els)[k]->get_assignments()->begin(),
                                (*els)[k]->get_assignments()->end());
                        new_assignments->push_back(tmpass);
                        logic_expression *tmplexp = new logic_expression(0,
                                newvar, new enum_value(s));
                        bool_expression *tmpbexp = new bool_expression(0,
                                tmplexp);
                        new_condition = new bool_expression(1,
                                (*els)[k]->get_condition(), tmpbexp);
                        evolution_line* newline = new evolution_line(
                                new_assignments, new_condition);
                        newels->push_back(newline);
                    }
                els = newels;
            }
        }
    }
    return els;
}

basic_agent::basic_agent(string *n, map<string, variable*> *lv, map<string,
        basictype *> *v0, map<string, basictype *> *v1, bool_expression *r,
        set<string> *v2, vector<protocol_line *> *v3,
        vector<evolution_line *> *v4)
{
    name = n;
    lobsvars = lv;
    obsvars = v0;
    vars = v1;
    actions = v2;
    protocol = v3;
    evolution = v4;
    redstates = r;
    action_indices = new map<string, vector<bool>*> ;
    generate_action_bdd_value();
}
basic_agent::~basic_agent()
{
    cout << "deleting basic_agent " << to_string() << endl;
    //delete vars;
    //delete actions;
    //delete protocol;
    //delete evolution;
    //delete redstates;
}
string basic_agent::get_name()
{
    if (name == NULL)
    {
        cout << " error: name in agent is undefined!" << endl;
        exit(1);
    }
    else
        return *name;
}
string* basic_agent::get_name_point()
{
    return name;
}
map<string, basictype *>* basic_agent::get_obsvars()
{
    return obsvars;
}
map<string, variable *>* basic_agent::get_lobsvars()
{
    return lobsvars;
}
map<string, basictype *>* basic_agent::get_vars()
{
    return vars;
}
basictype* basic_agent::get_basictype_by_name(string varname)
{
    if (obsvars != NULL)
    {
        if (obsvars->find(varname) != obsvars->end())
            return (*obsvars)[varname];
    }
    if (vars != NULL)
    {
        if (vars->find(varname) != vars->end())
            return (*vars)[varname];
    }
    return NULL;
}
set<string>* basic_agent::get_actions()
{
    return actions;
}
vector<protocol_line *>* basic_agent::get_protocol()
{
    return protocol;
}
vector<evolution_line *>* basic_agent::get_evolution()
{
    return evolution;
}
bool_expression* basic_agent::get_redstates()
{
    return redstates;
}
string basic_agent::to_string()
{
    string str = "Agent " + *name + "\n";

    if (obsvars != NULL && obsvars->size() > 0)
    {
        str += "Obsvars:\n";
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
            str += "    " + (*i).second->to_string() + ";\n";
        str += "end Obsvars\n";
    }

    str += "Vars:\n";
    for (map<string, basictype *>::iterator i = vars->begin(); i != vars->end(); i++)
        str += "    " + (*i).second->to_string() + ";\n";
    str += "end Vars\nRedStates:\n    ";
    if (redstates == NULL)
        str += "";
    else
        str += redstates->to_string() + ";";
    str += "\nend RedStates\nActions = { ";
    unsigned int k = 0;
    unsigned int bound = (unsigned int) actions->size() - 1;
    for (set<string>::iterator i = actions->begin(); i != actions->end(); i++)
    {
        if (k == bound)
            str += *i + " ";
        else
            str += *i + ", ";
        k++;
    }
    str += "}\nProtocol:\n";
    for (vector<protocol_line *>::iterator i = protocol->begin(); i
            != protocol->end(); i++)
        str += "    " + (*i)->to_string() + ";\n";
    str += "end Protocol\nEvolution:\n";
    for (vector<evolution_line *>::iterator i = evolution->begin(); i
            != evolution->end(); i++)
        str += "    " + (*i)->to_string() + ";\n";
    str += "end Evolution\n";
    str += "end Agent\n";
    return str;
}

int basic_agent::state_BDD_length()
{
    int count = 0;
    count += obsvars_BDD_length();
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
            count += (*i).second->BDD_length();
    return count;
}

int basic_agent::obsvars_BDD_length()
{
    int count = 0;
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
            count += (*i).second->BDD_length();
    return count;
}

unsigned int basic_agent::actions_BDD_length()
{
    if (actions == NULL || actions->size() == 0)
        return 0;
    return log_2(actions->size());
}

void basic_agent::set_action_index_begin(int i)
{
    action_index_begin = i;
}

void basic_agent::set_action_index_end(int i)
{
    action_index_end = i;
}

void basic_agent::set_var_index_begin(int i)
{
    var_index_begin = i;
}

void basic_agent::set_var_index_end(int i)
{
    var_index_end = i;
}

int basic_agent::get_action_index_begin()
{
    return action_index_begin;
}

int basic_agent::get_action_index_end()
{
    return action_index_end;
}

int basic_agent::get_var_index_begin()
{
    return var_index_begin;
}

int basic_agent::get_var_index_end()
{
    return var_index_end;
}

void basic_agent::generate_action_bdd_value()
{
    int size = actions_BDD_length();
    if (size == 0)
        return;
    vector<bool> base(size, false);
    for (set<string>::iterator i = actions->begin(); i != actions->end(); i++)
    {
        vector<bool> *temp = new vector<bool> (base);
        pair<string, vector<bool>*> p(*i, temp);
        action_indices->insert(p);
        for (int j = size - 1; j >= 0; j--)
        {
            if (base[j])
                base[j] = false;
            else
            {
                base[j] = true;
                break;
            }
        }
    }
}
void basic_agent::print_value_index()
{
    for (map<string, vector<bool>*>::iterator i = action_indices->begin(); i
            != action_indices->end(); i++)
    {
        cout << i->first << ": ";
        for (unsigned int j = 0; j < i->second->size(); j++)
            cout << ((*(i->second))[j] ? 1 : 0);
        cout << endl;
    }
}

map<string, vector<bool>*>* basic_agent::get_action_indices()
{
    return action_indices;
}

int basic_agent::allocate_BDD_2_variables(int start)
{
    set_var_index_begin(start);
    int count = start;
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            int l = (*i).second->BDD_length();
            (*i).second->set_index_begin(count);
            (*i).second->set_index_end(count + l - 1);
            count += l;
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            int l = (*i).second->BDD_length();
            (*i).second->set_index_begin(count);
            (*i).second->set_index_end(count + l - 1);
            count += l;
        }
    set_var_index_end(count - 1);
    return count;
}

int basic_agent::allocate_BDD_2_actions(int start)
{
    set_action_index_begin(start);
    int end = start + actions_BDD_length();
    set_action_index_end(end - 1);
    return end;
}

BDD basic_agent::encode_action(string act)
{
    map<string, vector<bool>*>::iterator k = action_indices->find(act);
    if (k != action_indices->end())
    {
        BDD temp = bddmgr->bddOne();
        vector<bool>* b = (*k).second;
        for (int i = action_index_begin; i <= action_index_end; i++)
            temp = temp * ((*b)[i - action_index_begin] ? (*a)[i] : !(*a)[i]);
        return temp;
    }
    return bddmgr->bddZero();
}

BDD basic_agent::encode_protocol()
{
    BDD bddprot = bddmgr->bddZero();
    BDD nullaction = bddmgr->bddOne();
    if (protocol->size() == 0)
        return bddmgr->bddOne();
    for (vector<protocol_line *>::iterator i = protocol->begin(); i
            != protocol->end(); i++)
    {
        bool_expression* condition = (*i)->get_condition();
        //bool_expression newcond = condition->push_negation_inside();
        //BDD tmpcond = newcond.encode_bdd(v, bddmgr->bddOne());
        BDD tmpcond = bddmgr->bddOne();
        if (!condition->is_other_branch())
        {
            tmpcond = condition->encode_bdd(bddOne);
            nullaction = nullaction * !tmpcond;
        }
        else
            tmpcond = nullaction;

        BDD tmpact = bddmgr->bddZero();
        //vector< BDD > *listoftmpact = new vector<BDD>;
        set<string> *actions = (*i)->get_actions();
        for (set<string>::iterator j = actions->begin(); j != actions->end(); j++)
        {
            //listoftmpact->push_back(encode_action(*j, a, bddmgr));
            tmpact = tmpact + encode_action(*j);
        }
        //tmpact = xorlist(listoftmpact);
        //listoftmpact->clear();
        //delete(listoftmpact);

        BDD oneline = tmpcond * tmpact;

        if (options["debug"] == 1 && options["verbosity"] > 9)
        {
            cout << (*i)->to_string() << "' : ";
            oneline.print(2, 2);
        }

        bddprot = bddprot + oneline;
    }
    //nullaction = nullaction * encode_action("null_action", a, bddmgr);

    //bddprot = bddprot + nullaction;
    return bddprot;
}

BDD basic_agent::encode_evolution()
{
    BDD bddevol = bddmgr->bddZero();
    BDD lastcond = bddmgr->bddOne();

    for (vector<evolution_line *>::iterator i = evolution->begin(); i
            != evolution->end(); i++)
    {
        vector<assignment *> *assignments = (*i)->get_assignments();
        map<string, basictype *> *mp = new map<string, basictype *> ;
        if (obsvars != NULL)
            for (map<string, basictype *>::iterator j = obsvars->begin(); j
                    != obsvars->end(); j++)
            {
                bool found = false;
                for (unsigned int k = 0; k < assignments->size(); k++)
                {
                    variable* var = (*assignments)[k]->get_var();
                    string varname = var->get_variable_name();
                    //cout << "varname = " << varname << ", j->first = " << j->first << endl;
                    if (varname == j->first)
                    {
                        found = true;
                        break;
                    }
                }

                if (!found) // we add this variable to both sides
                    mp->insert(*j);
            }

        if (vars != NULL)
            for (map<string, basictype *>::iterator j = vars->begin(); j
                    != vars->end(); j++)
            {
                bool found = false;
                for (unsigned int k = 0; k < assignments->size(); k++)
                {
                    variable* var = (*assignments)[k]->get_var();
                    string varname = var->get_variable_name();
                    //cout << "varname = " << varname << ", j->first = " << j->first << endl;
                    if (varname == j->first)
                    {
                        found = true;
                        break;
                    }
                }

                if (!found) // we add this variable to both sides
                    mp->insert(*j);
            }

        BDD bddassignment = (*i)->encode_bdd_assignements();
        BDD bddcondition = (*i)->encode_bdd_condition();
        for (map<string, basictype *>::iterator j = mp->begin(); j != mp->end(); j++)
        {
            int begin = j->second->get_index_begin();
            int end = j->second->get_index_end();
            //cout << "unchanged variable: " << j->first << endl;
            for (int k = begin; k <= end; k++)
                bddassignment
                        *= ((!(*v)[k] + (*pv)[k]) * ((*v)[k] + !(*pv)[k]));
        }
        lastcond = lastcond * !bddcondition;

        BDD oneline = bddassignment * bddcondition;

        if (options["debug"] == 1 && options["verbosity"] > 9)
        {
            cout << "encoding evolution '" << (*i)->to_string() << "' : ";
            //cout.flush();
            oneline.print(2, 2);
        }

        bddevol = bddevol + oneline;
        /*vector<evolution_line *> *els = (*i)->extend_to_all_variables(vars);
         for(vector<evolution_line*>::iterator k=els->begin(); k!=els->end(); k++) {
         BDD bddassignment = (*k)->encode_bdd_assignements(pv, bddmgr->bddOne());
         BDD bddcondition = (*k)->encode_bdd_condition(v, a, bddmgr->bddOne());
         //cout << (*i)->get_condition()->to_string();
         //bddcondition.print(2, 2);

         lastcond = lastcond * !bddcondition;

         BDD oneline = bddassignment * bddcondition;

         //cout << (*k)->to_string();
         //oneline.print(2, 2);

         bddevol = bddevol + oneline;
         }*/
    }

    BDD dnc = bddmgr->bddOne();
    int begin, end;
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            basictype *var_type = (*i).second;
            begin = var_type->get_index_begin();
            end = var_type->get_index_end();
            for (int j = begin; j <= end; j++)
                dnc = dnc * ((!(*v)[j] + (*pv)[j]) * ((*v)[j] + !(*pv)[j]));
        }
    if (vars != NULL)
    {
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            basictype *var_type = (*i).second;
            begin = var_type->get_index_begin();
            end = var_type->get_index_end();
            for (int j = begin; j <= end; j++)
                dnc = dnc * ((!(*v)[j] + (*pv)[j]) * ((*v)[j] + !(*pv)[j]));
        }
    }
    lastcond *= dnc;

    return bddevol + lastcond;
}

BDD basic_agent::encode_greenstates()
{
    if (redstates == NULL)
        return bddmgr->bddOne();
    else
    {
        BDD tmp = redstates->encode_bdd(bddOne);
        return (!tmp).SwapVariables(*v, *pv);
    }
}

void basic_agent::print_variable_BDD_encoding()
{
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            int begin = i->second->get_index_begin();
            int end = i->second->get_index_end();
            cout << "----- " << i->first << ": " << begin << " .. " << end
                    << " -----" << endl;
            basictype *b = i->second;
            if (b->get_type() == 2) //rangeint
                ((rangedint *) b)->print_value_index();
            else if (b->get_type() == 3) //enumerate
                ((enumerate *) b)->print_value_index();
            else
                b->print_value_index();
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            int begin = i->second->get_index_begin();
            int end = i->second->get_index_end();
            cout << "----- " << i->first << ": " << begin << " .. " << end
                    << " -----" << endl;
            basictype *b = i->second;
            if (b->get_type() == 2) //rangeint
                ((rangedint *) b)->print_value_index();
            else if (b->get_type() == 3) //enumerate
                ((enumerate *) b)->print_value_index();
            else
                b->print_value_index();
        }
}

void basic_agent::print_state(string prefix, BDD state, BDDvector v)
{
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            i->second->print_state(prefix, state, v);
            cout << endl;
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            i->second->print_state(prefix, state, v);
            cout << endl;
        }
}

bool basic_agent::is_valid_state(BDD state, BDDvector v)
{
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            if (!i->second->is_valid_state(state, v))
                return false;
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            if (!i->second->is_valid_state(state, v))
                return false;
        }
    return true;
}

void basic_agent::print_action(BDD state, BDDvector a)
{
    vector<bool> index;
    for (int i = action_index_begin; i <= action_index_end; i++)
        if (state <= a[i])
            index.push_back(true);
        else
            index.push_back(false);
    for (map<string, vector<bool>*>::iterator i = action_indices->begin(); i
            != action_indices->end(); i++)
    {
        bool flag = true;
        for (unsigned int j = 0; j < i->second->size(); j++)
            if ((*(i->second))[j] != index[j])
            {
                flag = false;
                break;
            }
        if (flag)
        {
            cout << i->first;
            return;
        }
    }
}

bool basic_agent::is_valid_action(BDD state, BDDvector a)
{
    if (action_indices->size() == 0)
        return true;
    vector<bool> index;
    for (int i = action_index_begin; i <= action_index_end; i++)
        if (state <= a[i])
            index.push_back(true);
        else
            index.push_back(false);
    for (map<string, vector<bool>*>::iterator i = action_indices->begin(); i
            != action_indices->end(); i++)
    {
        bool flag = true;
        for (unsigned int j = 0; j < i->second->size(); j++)
            if ((*(i->second))[j] != index[j])
            {
                flag = false;
                break;
            }
        if (flag)
        {
            return true;
        }
    }
    return false;
}

set<string>* basic_agent::get_obs_enum_values()
{
    if (obsvars != NULL)
    {
        set<string>* tmpset = new set<string> ;
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
            if (i->second->get_type() == 3)
            {
                set<string>* varset =
                        ((enumerate*) (i->second))->get_enumvalue();
                tmpset->insert(varset->begin(), varset->end());
            }
        return tmpset;
    }
    return NULL;
}

bool basic_agent::check_var_against_enum_values(set<string>* obsenum)
{
    bool flag = true;
    set<string>* tmpset = new set<string> ;
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
            if (i->second->get_type() == 3)
            {
                set<string>* varset =
                        ((enumerate*) (i->second))->get_enumvalue();
                tmpset->insert(varset->begin(), varset->end());
            }
    if (obsenum != NULL)
        tmpset->insert(obsenum->begin(), obsenum->end());
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
            if (tmpset->find(i->first) != tmpset->end())
            {
                flag = false;
                cout << "variable " << i->first
                        << " has been used as a enumerate value." << endl;
            }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
            if (tmpset->find(i->first) != tmpset->end())
            {
                flag = false;
                cout << "variable " << i->first
                        << " has been used as a enumerate value." << endl;
            }
    return flag;
}

bool basic_agent::check_lobsvars(map<string, basictype*>* envars)
{
    if (lobsvars != NULL && lobsvars->size() > 0)
        for (map<string, variable *>::iterator i = lobsvars->begin(); i
                != lobsvars->end(); i++)
        {
            map<string, basictype *>::iterator j;
            if (envars != NULL && (j = envars->find(i->first)) != envars->end())
                i->second->set_var_type(j->second);
            else
            {
                cout << "local observable variable " << i->first
                        << " is not defined in the environment." << endl;
                return false;
            }
        }
    return true;
}

// HERE

void basic_agent::print_stateXML(ofstream* myfile, BDD state, BDDvector v)
{
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            i->second->print_stateXML(myfile, state, v);
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            i->second->print_stateXML(myfile, state, v);
        }
}

void basic_agent::print_actionXML(ofstream* myfile, BDD state, BDDvector a)
{
    vector<bool> index;
    for (int i = action_index_begin; i <= action_index_end; i++)
        if (state <= a[i])
            index.push_back(true);
        else
            index.push_back(false);
    for (map<string, vector<bool>*>::iterator i = action_indices->begin(); i
            != action_indices->end(); i++)
    {
        bool flag = true;
        for (unsigned int j = 0; j < i->second->size(); j++)
            if ((*(i->second))[j] != index[j])
            {
                flag = false;
                break;
            }
        if (flag)
        {
            cout << i->first;
            return;
        }
    }
}

string basic_agent::state_to_str(BDD state, BDDvector v)
{
    ostringstream s;
    if (obsvars != NULL)
        for (map<string, basictype *>::iterator i = obsvars->begin(); i
                != obsvars->end(); i++)
        {
            s << "    " << i->second->state_to_str(state, v) << "\n";
        }
    if (vars != NULL)
        for (map<string, basictype *>::iterator i = vars->begin(); i
                != vars->end(); i++)
        {
            s << "    " << i->second->state_to_str(state, v) << "\n";
        }
    return s.str();
}

string basic_agent::action_to_str(BDD state, BDDvector a)
{
    ostringstream s;
    vector<bool> index;
    for (int i = action_index_begin; i <= action_index_end; i++)
        if (state <= a[i])
            index.push_back(true);
        else
            index.push_back(false);
    for (map<string, vector<bool>*>::iterator i = action_indices->begin(); i
            != action_indices->end(); i++)
    {
        bool flag = true;
        for (unsigned int j = 0; j < i->second->size(); j++)
            if ((*(i->second))[j] != index[j])
            {
                flag = false;
                break;
            }
        if (flag)
        {
            s << i->first;
        }
    }
    return s.str();
}

BDD basic_agent::project_local_state(BDD *state, BDDvector* v)
{
    BDD tmp = bddmgr->bddOne(); // Always true

    if (lobsvars != NULL && lobsvars->size() > 0)
    {
        map<string, basictype*>* envars = (*agents)[0]->get_vars();
        for (map<string, basictype *>::iterator i = envars->begin(); i
                != envars->end(); i++)
        {
            if (lobsvars->find(i->first) == lobsvars->end()) // i->first is not local observable variable
            {
                basictype* bt = i->second;
                unsigned char bt_type = bt->get_type();
                int index_begin, index_end;
                if (bt_type == 1) // boolean
                {
                    index_begin = bt->get_index_begin();
                    index_end = bt->get_index_begin();
                }
                else if (bt_type == 2) // ranged int
                {
                    index_begin = ((rangedint*) bt)->get_index_begin();
                    index_end = ((rangedint*) bt)->get_index_begin();
                }
                else // enumerate
                {
                    index_begin = ((enumerate*) bt)->get_index_begin();
                    index_end = ((enumerate*) bt)->get_index_begin();
                }
                for (int j = index_begin; j <= index_end; j++)
                    tmp = tmp * (*v)[j];
            }
        }
        for (int j = envars_bdd_length; j < get_var_index_begin(); j++)
        {
            tmp = tmp * (*v)[j];
        }
    }
    else
    {
        for (int j = obsvars_bdd_length; j < get_var_index_begin(); j++)
        {
            tmp = tmp * (*v)[j];
        }
    }

    for (int j = get_var_index_end() + 1; j < v->count(); j++)
    {
        tmp = tmp * (*v)[j];
    }

    return state->ExistAbstract(tmp);
}

/**********************************************
 transition (for counterexamples)
 **********************************************/
transition::transition(BDD *fr, int frid, BDD *t, int tid, BDD* lab)
{
    from = new BDD((*fr));
    fromid = frid;
    to = new BDD((*t));
    toid = tid;
    //type = ty;
    label = new BDD((*lab));

    temporal = true;
    epistemic1 = "";
    epistemic2 = "";
}
transition::transition(BDD *fr, int frid, BDD *t, int tid, string name1,
        BDD* lab)
{
    from = new BDD((*fr));
    fromid = frid;
    to = new BDD((*t));
    toid = tid;
    //type = ty;
    label = new BDD((*lab));

    temporal = false;
    epistemic1 = name1;
    epistemic2 = "";
}
transition::transition(BDD *fr, int frid, BDD *t, int tid, string name1,
        string name2, BDD* lab)
{
    from = new BDD((*fr));
    fromid = frid;
    to = new BDD((*t));
    toid = tid;
    //type = ty;
    label = new BDD((*lab));

    temporal = false;
    epistemic1 = name1;
    epistemic2 = name2;
}

transition::transition()
{
    from = new BDD();
    fromid = -1;
    to = new BDD();
    toid = -1;
    //type = -1;
    label = new BDD();

    temporal = false;
    epistemic1 = "";
    epistemic2 = "";
}

transition::~transition()
{
    // do nothing
}

BDD * transition::getfrom()
{
    return from;
}

BDD * transition::getto()
{
    return to;
}

BDD * transition::getlabel()
{
    return label;
}

int transition::getfromid()
{
    return fromid;
}

int transition::gettoid()
{
    return toid;
}

/* int transition::gettype() {
 return type;
 }*/

void transition::setfrom(BDD * fr)
{
    from = fr;
}

void transition::setto(BDD * fr)
{
    to = fr;
}

void transition::setlabel(BDD * fr)
{
    label = fr;
}

void transition::setfromid(int frid)
{
    fromid = frid;
}

void transition::settoid(int frid)
{
    toid = frid;
}

/* void transition::settype(int frid) {
 type = frid;
 } */

void transition::print()
{
    cout << "------- Transition --------" << endl;
    //cout << " Type: " << type << endl;
    cout << " From (id): " << fromid << endl;
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        cout << "    Agent " << (*agents)[i]->get_name() << endl;
        (*agents)[i]->print_state("  ", *from, *v);
    }

    cout << " To (id): " << toid << endl;
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        cout << "    Agent " << (*agents)[i]->get_name() << endl;
        (*agents)[i]->print_state("  ", *to, *v);
    }

    if (isTemporal())
    {
        cout << " Joint action: " << endl;
        for (unsigned int i = 0; i < agents->size(); i++)
        {
            cout << (*agents)[i]->get_name() << " : ";
            (*agents)[i]->print_action(*label, *a);
            if (i < agents->size() - 1)
                cout << "; ";
            else
                cout << endl;
        }
    }

    cout << "---------------------------" << endl;
}

void transition::printXML(ofstream *myfile)
{
    *myfile << "  <transition>\n";
    //*myfile << "    <type>" << type << "</type>\n";
    *myfile << "    <from-id>" << fromid << "</from-id>\n";
    *myfile << "    <to-id>" << toid << "</to-id>\n";
    *myfile << "    <from>\n";
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        *myfile << "      <agent name=\"" << (*agents)[i]->get_name()
                << "\">\n";
        (*agents)[i]->print_stateXML(myfile, *from, *v);
        *myfile << "      </agent>\n";
    }
    *myfile << "    </from>\n";
    *myfile << "    <to>\n";
    for (unsigned int i = 0; i < agents->size(); i++)
    {
        *myfile << "      <agent name=\"" << (*agents)[i]->get_name()
                << "\">\n";
        (*agents)[i]->print_stateXML(myfile, *to, *v);
        *myfile << "      </agent>\n";
    }
    *myfile << "    </to>\n";
    *myfile << "  </transition>\n";

}

void transition::to_str(ofstream *myfile)
{
    *myfile << "    " << fromid << " -> " << toid;

    if (isTemporal())
    {
        // A temporal transition

        // HERE
        *myfile << "[label=\"<";
        for (unsigned int i = 0; i < agents->size(); i++)
        {
            string act_str = (*agents)[i]->action_to_str(*label, *a);
            if (act_str != "")
            {
                *myfile << act_str;
                if (!(i == agents->size() - 1))
                {
                    *myfile << ";";
                }
            }
        }
        *myfile << ">\"]" << endl;
    }
    else
    {
        //*myfile << "[label=\"" << (*agents)[-type]->get_name() << "\", style=dotted]"<< endl;
        *myfile << "[label=\"" << epistemic1
                << (epistemic2.empty() ? "" : ", ") << epistemic2
                << "\", style=dotted]" << endl;
    }
}

bool transition::isTemporal()
{
    return temporal;
}

string transition::getEpistemic1()
{
    return epistemic1;
}

string transition::getEpistemic2()
{
    return epistemic2;
}

/*
 * end transition
 */
